set X = { A where A is Subset of F_{2}() : ex K being strict StableSubgroup of F_{2}() st

( A = the carrier of K & P_{1}[K] ) } ;

consider T being strict StableSubgroup of F_{2}() such that

A2: P_{1}[T]
by A1;

A3: carr T in { A where A is Subset of F_{2}() : ex K being strict StableSubgroup of F_{2}() st

( A = the carrier of K & P_{1}[K] ) }
by A2;

then reconsider Y = meet { A where A is Subset of F_{2}() : ex K being strict StableSubgroup of F_{2}() st

( A = the carrier of K & P_{1}[K] ) } as Subset of F_{2}() by SETFAM_1:7;

hence ex H being strict StableSubgroup of F_{2}() st the carrier of H = meet { A where A is Subset of F_{2}() : ex K being strict StableSubgroup of F_{2}() st

( A = the carrier of K & P_{1}[K] ) }
by A10, A4, A18, Lm14; :: thesis: verum

( A = the carrier of K & P

consider T being strict StableSubgroup of F

A2: P

A3: carr T in { A where A is Subset of F

( A = the carrier of K & P

then reconsider Y = meet { A where A is Subset of F

( A = the carrier of K & P

A4: now :: thesis: for a being Element of F_{2}() st a in Y holds

a " in Y

a " in Y

let a be Element of F_{2}(); :: thesis: ( a in Y implies a " in Y )

assume A5: a in Y ; :: thesis: a " in Y

end;assume A5: a in Y ; :: thesis: a " in Y

now :: thesis: for Z being set st Z in { A where A is Subset of F_{2}() : ex K being strict StableSubgroup of F_{2}() st

( A = the carrier of K & P_{1}[K] ) } holds

a " in Z

hence
a " in Y
by A3, SETFAM_1:def 1; :: thesis: verum( A = the carrier of K & P

a " in Z

let Z be set ; :: thesis: ( Z in { A where A is Subset of F_{2}() : ex K being strict StableSubgroup of F_{2}() st

( A = the carrier of K & P_{1}[K] ) } implies a " in Z )

assume A6: Z in { A where A is Subset of F_{2}() : ex K being strict StableSubgroup of F_{2}() st

( A = the carrier of K & P_{1}[K] ) }
; :: thesis: a " in Z

then consider A being Subset of F_{2}() such that

A7: A = Z and

A8: ex H being strict StableSubgroup of F_{2}() st

( A = the carrier of H & P_{1}[H] )
;

consider H being StableSubgroup of F_{2}() such that

A9: A = the carrier of H and

P_{1}[H]
by A8;

a in the carrier of H by A5, A6, A7, A9, SETFAM_1:def 1;

then a in H by STRUCT_0:def 5;

then a " in H by Lm19;

hence a " in Z by A7, A9, STRUCT_0:def 5; :: thesis: verum

end;( A = the carrier of K & P

assume A6: Z in { A where A is Subset of F

( A = the carrier of K & P

then consider A being Subset of F

A7: A = Z and

A8: ex H being strict StableSubgroup of F

( A = the carrier of H & P

consider H being StableSubgroup of F

A9: A = the carrier of H and

P

a in the carrier of H by A5, A6, A7, A9, SETFAM_1:def 1;

then a in H by STRUCT_0:def 5;

then a " in H by Lm19;

hence a " in Z by A7, A9, STRUCT_0:def 5; :: thesis: verum

A10: now :: thesis: for a, b being Element of F_{2}() st a in Y & b in Y holds

a * b in Y

a * b in Y

let a, b be Element of F_{2}(); :: thesis: ( a in Y & b in Y implies a * b in Y )

assume that

A11: a in Y and

A12: b in Y ; :: thesis: a * b in Y

end;assume that

A11: a in Y and

A12: b in Y ; :: thesis: a * b in Y

now :: thesis: for Z being set st Z in { A where A is Subset of F_{2}() : ex K being strict StableSubgroup of F_{2}() st

( A = the carrier of K & P_{1}[K] ) } holds

a * b in Z

hence
a * b in Y
by A3, SETFAM_1:def 1; :: thesis: verum( A = the carrier of K & P

a * b in Z

let Z be set ; :: thesis: ( Z in { A where A is Subset of F_{2}() : ex K being strict StableSubgroup of F_{2}() st

( A = the carrier of K & P_{1}[K] ) } implies a * b in Z )

assume A13: Z in { A where A is Subset of F_{2}() : ex K being strict StableSubgroup of F_{2}() st

( A = the carrier of K & P_{1}[K] ) }
; :: thesis: a * b in Z

then consider A being Subset of F_{2}() such that

A14: A = Z and

A15: ex H being strict StableSubgroup of F_{2}() st

( A = the carrier of H & P_{1}[H] )
;

consider H being StableSubgroup of F_{2}() such that

A16: A = the carrier of H and

P_{1}[H]
by A15;

b in the carrier of H by A12, A13, A14, A16, SETFAM_1:def 1;

then A17: b in H by STRUCT_0:def 5;

a in the carrier of H by A11, A13, A14, A16, SETFAM_1:def 1;

then a in H by STRUCT_0:def 5;

then a * b in H by A17, Lm18;

hence a * b in Z by A14, A16, STRUCT_0:def 5; :: thesis: verum

end;( A = the carrier of K & P

assume A13: Z in { A where A is Subset of F

( A = the carrier of K & P

then consider A being Subset of F

A14: A = Z and

A15: ex H being strict StableSubgroup of F

( A = the carrier of H & P

consider H being StableSubgroup of F

A16: A = the carrier of H and

P

b in the carrier of H by A12, A13, A14, A16, SETFAM_1:def 1;

then A17: b in H by STRUCT_0:def 5;

a in the carrier of H by A11, A13, A14, A16, SETFAM_1:def 1;

then a in H by STRUCT_0:def 5;

then a * b in H by A17, Lm18;

hence a * b in Z by A14, A16, STRUCT_0:def 5; :: thesis: verum

A18: now :: thesis: for o being Element of F_{1}()

for a being Element of F_{2}() st a in Y holds

(F_{2}() ^ o) . a in Y

for a being Element of F

(F

let o be Element of F_{1}(); :: thesis: for a being Element of F_{2}() st a in Y holds

(F_{2}() ^ o) . a in Y

let a be Element of F_{2}(); :: thesis: ( a in Y implies (F_{2}() ^ o) . a in Y )

assume A19: a in Y ; :: thesis: (F_{2}() ^ o) . a in Y

_{2}() ^ o) . a in Y
by A3, SETFAM_1:def 1; :: thesis: verum

end;(F

let a be Element of F

assume A19: a in Y ; :: thesis: (F

now :: thesis: for Z being set st Z in { A where A is Subset of F_{2}() : ex K being strict StableSubgroup of F_{2}() st

( A = the carrier of K & P_{1}[K] ) } holds

(F_{2}() ^ o) . a in Z

hence
(F( A = the carrier of K & P

(F

let Z be set ; :: thesis: ( Z in { A where A is Subset of F_{2}() : ex K being strict StableSubgroup of F_{2}() st

( A = the carrier of K & P_{1}[K] ) } implies (F_{2}() ^ o) . a in Z )

assume A20: Z in { A where A is Subset of F_{2}() : ex K being strict StableSubgroup of F_{2}() st

( A = the carrier of K & P_{1}[K] ) }
; :: thesis: (F_{2}() ^ o) . a in Z

then consider A being Subset of F_{2}() such that

A21: A = Z and

A22: ex H being strict StableSubgroup of F_{2}() st

( A = the carrier of H & P_{1}[H] )
;

consider H being StableSubgroup of F_{2}() such that

A23: A = the carrier of H and

P_{1}[H]
by A22;

a in the carrier of H by A19, A20, A21, A23, SETFAM_1:def 1;

then a in H by STRUCT_0:def 5;

then (F_{2}() ^ o) . a in H
by Lm9;

hence (F_{2}() ^ o) . a in Z
by A21, A23, STRUCT_0:def 5; :: thesis: verum

end;( A = the carrier of K & P

assume A20: Z in { A where A is Subset of F

( A = the carrier of K & P

then consider A being Subset of F

A21: A = Z and

A22: ex H being strict StableSubgroup of F

( A = the carrier of H & P

consider H being StableSubgroup of F

A23: A = the carrier of H and

P

a in the carrier of H by A19, A20, A21, A23, SETFAM_1:def 1;

then a in H by STRUCT_0:def 5;

then (F

hence (F

now :: thesis: for Z being set st Z in { A where A is Subset of F_{2}() : ex K being strict StableSubgroup of F_{2}() st

( A = the carrier of K & P_{1}[K] ) } holds

1_ F_{2}() in Z

then
Y <> {}
by A3, SETFAM_1:def 1;( A = the carrier of K & P

1_ F

let Z be set ; :: thesis: ( Z in { A where A is Subset of F_{2}() : ex K being strict StableSubgroup of F_{2}() st

( A = the carrier of K & P_{1}[K] ) } implies 1_ F_{2}() in Z )

assume Z in { A where A is Subset of F_{2}() : ex K being strict StableSubgroup of F_{2}() st

( A = the carrier of K & P_{1}[K] ) }
; :: thesis: 1_ F_{2}() in Z

then consider A being Subset of F_{2}() such that

A24: Z = A and

A25: ex K being strict StableSubgroup of F_{2}() st

( A = the carrier of K & P_{1}[K] )
;

consider H being StableSubgroup of F_{2}() such that

A26: A = the carrier of H and

P_{1}[H]
by A25;

1_ F_{2}() in H
by Lm17;

hence 1_ F_{2}() in Z
by A24, A26, STRUCT_0:def 5; :: thesis: verum

end;( A = the carrier of K & P

assume Z in { A where A is Subset of F

( A = the carrier of K & P

then consider A being Subset of F

A24: Z = A and

A25: ex K being strict StableSubgroup of F

( A = the carrier of K & P

consider H being StableSubgroup of F

A26: A = the carrier of H and

P

1_ F

hence 1_ F

hence ex H being strict StableSubgroup of F

( A = the carrier of K & P