set X = { A where A is Subset of F₂() : ex K being strict StableSubgroup of F₂() st
( A = the carrier of K & P₁[K] ) } ;
consider T being strict StableSubgroup of F₂() such that
A2: P₁[T] by A1;
A3: carr T in { A where A is Subset of F₂() : ex K being strict StableSubgroup 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 StableSubgroup 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 StableSubgroup 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 StableSubgroup 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 StableSubgroup of F₂() st
( A = the carrier of K & P₁[K] ) ;
consider H being StableSubgroup of F₂() such that
A6: ( A = the carrier of H & P₁[H] ) by A5;
1_ F₂() in H by Lm18;
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 StableSubgroup 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 StableSubgroup 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 StableSubgroup of F₂() st
( A = the carrier of H & P₁[H] ) ;
consider H being StableSubgroup 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 Lm19;
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;

A14: now

let a be Element of F₂(); :: thesis: ( a in Y implies a " in Y )
assume A15: 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 StableSubgroup of F₂() st
( A = the carrier of K & P₁[K] ) } implies a " in Z )
assume A16: Z in { A where A is Subset of F₂() : ex K being strict StableSubgroup of F₂() st
( A = the carrier of K & P₁[K] ) } ; :: thesis: a " in Z
then consider A being Subset of F₂() such that
A17: A = Z and
A18: ex H being strict StableSubgroup of F₂() st
( A = the carrier of H & P₁[H] ) ;
consider H being StableSubgroup of F₂() such that
A19: ( A = the carrier of H & P₁[H] ) by A18;
a in the carrier of H by A15, A16, A17, A19, SETFAM_1:def 1;
then a in H by STRUCT_0:def 5;
then a " in H by Lm20;
hence a " in Z by A17, A19, STRUCT_0:def 5; :: thesis: verum

end;

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

end;

now

let o be Element of F₁(); :: thesis: for a being Element of F₂() st a in Y holds
(F₂() ^ o) . a in Y
let a be Element of F₂(); :: thesis: ( a in Y implies (F₂() ^ o) . a in Y )
assume A20: a in Y ; :: thesis: (F₂() ^ o) . a in Y

now

let Z be set ; :: thesis: ( Z in { A where A is Subset of F₂() : ex K being strict StableSubgroup of F₂() st
( A = the carrier of K & P₁[K] ) } implies (F₂() ^ o) . a in Z )
assume A21: Z in { A where A is Subset of F₂() : ex K being strict StableSubgroup of F₂() st
( A = the carrier of K & P₁[K] ) } ; :: thesis: (F₂() ^ o) . a in Z
then consider A being Subset of F₂() such that
A22: A = Z and
A23: ex H being strict StableSubgroup of F₂() st
( A = the carrier of H & P₁[H] ) ;
consider H being StableSubgroup of F₂() such that
A24: ( A = the carrier of H & P₁[H] ) by A23;
a in the carrier of H by A20, A21, A22, A24, SETFAM_1:def 1;
then a in H by STRUCT_0:def 5;
then (F₂() ^ o) . a in H by Lm10;
hence (F₂() ^ o) . a in Z by A22, A24, STRUCT_0:def 5; :: thesis: verum

end;

hence (F₂() ^ o) . a in Y by A3, SETFAM_1:def 1; :: thesis: verum

end;

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