set X = { A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] ) } ;
consider T being strict Subgroup of F1() such that
A2: P1[T] by A1;
A3: carr T in { A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] ) } by A2;
then reconsider Y = meet { A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] ) } as Subset of F1() by SETFAM_1:7;
A4: now :: thesis: for a being Element of F1() st a in Y holds
a " in Y
let a be Element of F1(); :: thesis: ( a in Y implies a " in Y )
assume A5: a in Y ; :: thesis: a " in Y
now :: thesis: for Z being set st Z in { A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] ) } holds
a " in Z
let Z be set ; :: thesis: ( Z in { A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] ) } implies a " in Z )
assume A6: Z in { A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] ) } ; :: thesis: a " in Z
then consider A being Subset of F1() such that
A7: A = Z and
A8: ex H being strict Subgroup of F1() st
( A = the carrier of H & P1[H] ) ;
consider H being Subgroup of F1() such that
A9: A = the carrier of H and
P1[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 GROUP_2:51;
hence a " in Z by A7, A9, STRUCT_0:def 5; :: thesis: verum
end;
hence a " in Y by A3, SETFAM_1:def 1; :: thesis: verum
end;
A10: now :: thesis: for a, b being Element of F1() st a in Y & b in Y holds
a * b in Y
let a, b be Element of F1(); :: 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
now :: thesis: for Z being set st Z in { A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] ) } holds
a * b in Z
let Z be set ; :: thesis: ( Z in { A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] ) } implies a * b in Z )
assume A13: Z in { A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] ) } ; :: thesis: a * b in Z
then consider A being Subset of F1() such that
A14: A = Z and
A15: ex H being strict Subgroup of F1() st
( A = the carrier of H & P1[H] ) ;
consider H being Subgroup of F1() such that
A16: A = the carrier of H and
P1[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, GROUP_2:50;
hence a * b in Z by A14, A16, STRUCT_0:def 5; :: thesis: verum
end;
hence a * b in Y by A3, SETFAM_1:def 1; :: thesis: verum
end;
now :: thesis: for Z being set st Z in { A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] ) } holds
1_ F1() in Z
let Z be set ; :: thesis: ( Z in { A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] ) } implies 1_ F1() in Z )
assume Z in { A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] ) } ; :: thesis: 1_ F1() in Z
then consider A being Subset of F1() such that
A18: Z = A and
A19: ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] ) ;
consider H being Subgroup of F1() such that
A20: A = the carrier of H and
P1[H] by A19;
1_ F1() in H by GROUP_2:46;
hence 1_ F1() in Z by A18, A20, STRUCT_0:def 5; :: thesis: verum
end;
then Y <> {} by A3, SETFAM_1:def 1;
hence ex H being strict Subgroup of F1() st the carrier of H = meet { A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] ) } by A10, A4, GROUP_2:52; :: thesis: verum