defpred S1[ set ] means ex H being Subgroup of G st
( $1 = carr H & A c= $1 );
consider X being set such that
A1: for Y being set holds
( Y in X iff ( Y in bool the carrier of G & S1[Y] ) ) from XFAMILY:sch 1();
 set M = meet X;
A2: carr ((Omega). G) = the carrier of ((Omega). G) ;
then A3: X <> {} by A1;
A4: the carrier of G in X by A1, A2;
A5: meet X c= the carrier of G by A4, SETFAM_1:def 1;
now :: thesis: for Y being set st Y in X holds
1_ G in Y
let Y be set ; :: thesis: ( Y in X implies 1_ G in Y )
assume Y in X ; :: thesis: 1_ G in Y
then consider H being Subgroup of G such that
A6: Y = carr H and
A c= Y by A1;
1_ G in H by GROUP_2:46;
hence 1_ G in Y by A6, STRUCT_0:def 5; :: thesis: verum
end;
then A7: meet X <> {} by A3, SETFAM_1:def 1;
reconsider M = meet X as Subset of G by A5;
A8: now :: thesis: for a, b being Element of G st a in M & b in M holds
a * b in M
let a, b be Element of G; :: thesis: ( a in M & b in M implies a * b in M )
assume A9: ( a in M & b in M ) ; :: thesis: a * b in M
now :: thesis: for Y being set st Y in X holds
a * b in Y
let Y be set ; :: thesis: ( Y in X implies a * b in Y )
assume A10: Y in X ; :: thesis: a * b in Y
then consider H being Subgroup of G such that
A11: Y = carr H and
A c= Y by A1;
( a in carr H & b in carr H ) by A9, A10, A11, SETFAM_1:def 1;
hence a * b in Y by A11, GROUP_2:74; :: thesis: verum
end;
hence a * b in M by A3, SETFAM_1:def 1; :: thesis: verum
end;
now :: thesis: for a being Element of G st a in M holds
a " in M
let a be Element of G; :: thesis: ( a in M implies a " in M )
assume A12: a in M ; :: thesis: a " in M
now :: thesis: for Y being set st Y in X holds
a " in Y
let Y be set ; :: thesis: ( Y in X implies a " in Y )
assume A13: Y in X ; :: thesis: a " in Y
then consider H being Subgroup of G such that
A14: Y = carr H and
A c= Y by A1;
a in carr H by A12, A13, A14, SETFAM_1:def 1;
hence a " in Y by A14, GROUP_2:75; :: thesis: verum
end;
hence a " in M by A3, SETFAM_1:def 1; :: thesis: verum
end;
then consider H being strict Subgroup of G such that
A15: the carrier of H = M by A7, A8, GROUP_2:52;
take H ; :: thesis: ( A c= the carrier of H & ( for H being strict Subgroup of G st A c= the carrier of H holds
H is Subgroup of H ) )
now :: thesis: for Y being set st Y in X holds
A c= Y
let Y be set ; :: thesis: ( Y in X implies A c= Y )
assume Y in X ; :: thesis: A c= Y
then ex H being Subgroup of G st
( Y = carr H & A c= Y ) by A1;
hence A c= Y ; :: thesis: verum
end;
hence A c= the carrier of H by A3, A15, SETFAM_1:5; :: thesis: for H being strict Subgroup of G st A c= the carrier of H holds
H is Subgroup of H
let H1 be strict Subgroup of G; :: thesis: ( A c= the carrier of H1 implies H is Subgroup of H1 )
A16: the carrier of H1 = carr H1 ;
assume A c= the carrier of H1 ; :: thesis: H is Subgroup of H1
then the carrier of H1 in X by A1, A16;
hence H is Subgroup of H1 by A15, GROUP_2:57, SETFAM_1:3; :: thesis: verum