Таким образом,

- решетка с дополнениями. Тогда, применяя лемму , получаем

Так как

то, в силу произвольности выбора группы

, получаем

Достаточность. Пусть теперь

. Пусть

- произвольная

-насыщенная формация, принадлежащая решетке

, т.е.

.
Обозначим через

множество всех минимальных

-насыщенных неразрешимых подформаций, содержащихся в

, а через

- множество всех минимальных

-насыщенных неразрешимых подформаций, не содержащихся в

. Очевидно, что множество

является дополнением к множеству

во множестве всех

-насыщенных неразрешимых подформаций, содержащихся в

. Пусть

-

-насыщенныя формация, порожденная множеством

, а

-

-насыщенная формация, порожденная множеством

. Поскольку

и

, то ввиду леммы имеют место равенства

Допустим, что

не содержится в

, то есть

. Тогда по лемме в

имеется минимальная

-насыщенная неразрешимая формация

. По лемме

для некоторого

. Следовательно,

. Но

. Противоречие. т.е.

. Но в таком случае

. Ввиду леммы и произвольности выбора формации

, каждый элемент решетки

представим в виде объединения содержащихся в нем атомов.
Покажем теперь, что в решетке

дополняема каждая

-насыщенная формация. Если

, то дополнением к

в решетке

является формация

. Итак, можем считать, что

. Обозначим через

множества всех атомов решетки

, через

- множества всех атомов решетки

, которые содержатся в

. Тогда

, иначе, ввиду доказанного выше,

Пусть

- дополнение к

в

и

Так как по условию

то ввиду леммы имеет место равенство

Рассмотрим формацию

. Так как

и

являются элементами решетки

, то

. Допустим, что

не содержится в

, т.е.

. Тогда по лемме формация

содержит минимальную

-насыщенную неразрешимую подформацию

. Следовательно,

содержит формацию

. По лемме формация

- атом решетки

, содержащийся в

. Так как

содержится в

, то, применяя теперь лемму , имеем

Полученное противоречие показывает, что

. Таким образом, формация

- дополнение к

в решетке

. А, следовательно,

- решетка с дополнениями. Теорема доказана.
Если

, то из теоремы вытекает
Пусть
- некоторая насыщенная неразрешимая формация и
- множество всех минимальных насыщенных неразрешимых подформаций из
. Тогда и только тогда
- решетка с дополнениями, когда