set X = { A where A is Subset of F₁() : ex K being strict Subgroup of F₁() st
( A = the carrier of K & P₁[K] ) } ;
consider T being strict Subgroup of F₁() such that
A2: P₁[T] by A1;
A3: carr T in { A where A is Subset of F₁() : ex K being strict Subgroup of F₁() st
( A = the carrier of K & P₁[K] ) } by A2;
then reconsider Y = meet { A where A is Subset of F₁() : ex K being strict Subgroup of F₁() st
( A = the carrier of K & P₁[K] ) } as Subset of F₁() by SETFAM_1:8;

now

let Z be set ; :: thesis: ( Z in { A where A is Subset of F₁() : ex K being strict Subgroup of F₁() st
( A = the carrier of K & P₁[K] ) } implies 1_ F₁() in Z )
assume Z in { A where A is Subset of F₁() : ex K being strict Subgroup of F₁() st
( A = the carrier of K & P₁[K] ) } ; :: thesis: 1_ F₁() in Z
then consider A being Subset of F₁() such that
A4: Z = A and
A5: ex K being strict Subgroup of F₁() st
( A = the carrier of K & P₁[K] ) ;
consider H being Subgroup of F₁() such that
A6: ( A = the carrier of H & P₁[H] ) by A5;
1_ F₁() in H by GROUP_2:55;
hence 1_ F₁() in Z by A4, A6, STRUCT_0:def 5; :: thesis: verum

end;

then A7: Y <> {} by A3, SETFAM_1:def 1;

A8: now

let a, b be Element of F₁(); :: thesis: ( a in Y & b in Y implies a * b in Y )
assume A9: ( a in Y & b in Y ) ; :: thesis: a * b in Y

now

let Z be set ; :: thesis: ( Z in { A where A is Subset of F₁() : ex K being strict Subgroup of F₁() st
( A = the carrier of K & P₁[K] ) } implies a * b in Z )
assume A10: Z in { A where A is Subset of F₁() : ex K being strict Subgroup of F₁() st
( A = the carrier of K & P₁[K] ) } ; :: thesis: a * b in Z
then consider A being Subset of F₁() such that
A11: A = Z and
A12: ex H being strict Subgroup of F₁() st
( A = the carrier of H & P₁[H] ) ;
consider H being Subgroup of F₁() such that
A13: ( A = the carrier of H & P₁[H] ) by A12;
( a in the carrier of H & b in the carrier of H ) by A9, A10, A11, A13, SETFAM_1:def 1;
then ( a in H & b in H ) by STRUCT_0:def 5;
then a * b in H by GROUP_2:59;
hence a * b in Z by A11, A13, STRUCT_0:def 5; :: thesis: verum

end;

hence a * b in Y by A3, SETFAM_1:def 1; :: thesis: verum

end;

now

let a be Element of F₁(); :: thesis: ( a in Y implies a " in Y )
assume A14: a in Y ; :: thesis: a " in Y

now

let Z be set ; :: thesis: ( Z in { A where A is Subset of F₁() : ex K being strict Subgroup of F₁() st
( A = the carrier of K & P₁[K] ) } implies a " in Z )
assume A15: Z in { A where A is Subset of F₁() : ex K being strict Subgroup of F₁() st
( A = the carrier of K & P₁[K] ) } ; :: thesis: a " in Z
then consider A being Subset of F₁() such that
A16: A = Z and
A17: ex H being strict Subgroup of F₁() st
( A = the carrier of H & P₁[H] ) ;
consider H being Subgroup of F₁() such that
A18: ( A = the carrier of H & P₁[H] ) by A17;
a in the carrier of H by A14, A15, A16, A18, SETFAM_1:def 1;
then a in H by STRUCT_0:def 5;
then a " in H by GROUP_2:60;
hence a " in Z by A16, A18, STRUCT_0:def 5; :: thesis: verum

end;

hence a " in Y by A3, SETFAM_1:def 1; :: thesis: verum

end;

hence ex H being strict Subgroup of F₁() st the carrier of H = meet { A where A is Subset of F₁() : ex K being strict Subgroup of F₁() st
( A = the carrier of K & P₁[K] ) } by A7, A8, GROUP_2:61; :: thesis: verum