defpred S1[ set ] means ex H being strict StableSubgroup 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 strict StableSubgroup of G such that
A6: Y = carr H and
A c= Y by A1;
1_ G in H by Lm17;
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 o being Element of O
for a being Element of G st a in M holds
(G ^ o) . a in M
let o be Element of O; :: thesis: for a being Element of G st a in M holds
(G ^ o) . a in M
let a be Element of G; :: thesis: ( a in M implies (G ^ o) . a in M )
assume A9: a in M ; :: thesis: (G ^ o) . a in M
now :: thesis: for Y being set st Y in X holds
(G ^ o) . a in Y
let Y be set ; :: thesis: ( Y in X implies (G ^ o) . a in Y )
assume A10: Y in X ; :: thesis: (G ^ o) . a in Y
then consider H being strict StableSubgroup of G such that
A11: Y = carr H and
A c= Y by A1;
a in carr H by A9, A10, A11, SETFAM_1:def 1;
then a in H by STRUCT_0:def 5;
then (G ^ o) . a in H by Lm9;
hence (G ^ o) . a in Y by A11, STRUCT_0:def 5; :: thesis: verum
end;
hence (G ^ o) . a in M by A3, SETFAM_1:def 1; :: thesis: verum
end;
A12: 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 that
A13: a in M and
A14: 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 A15: Y in X ; :: thesis: a * b in Y
then consider H being strict StableSubgroup of G such that
A16: Y = carr H and
A c= Y by A1;
b in carr H by A14, A15, A16, SETFAM_1:def 1;
then A17: b in H by STRUCT_0:def 5;
a in carr H by A13, A15, 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 Y by A16, STRUCT_0:def 5; :: 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 A18: 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 A19: Y in X ; :: thesis: a " in Y
then consider H being strict StableSubgroup of G such that
A20: Y = carr H and
A c= Y by A1;
a in carr H by A18, A19, A20, SETFAM_1:def 1;
then a in H by STRUCT_0:def 5;
then a " in H by Lm19;
hence a " in Y by A20, STRUCT_0:def 5; :: thesis: verum
end;
hence a " in M by A3, SETFAM_1:def 1; :: thesis: verum
end;
then consider H being strict StableSubgroup of G such that
A21: the carrier of H = M by A7, A12, A8, Lm14;
take H ; :: thesis: ( A c= the carrier of H & ( for H being strict StableSubgroup of G st A c= the carrier of H holds
H is StableSubgroup 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 strict StableSubgroup 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, A21, SETFAM_1:5; :: thesis: for H being strict StableSubgroup of G st A c= the carrier of H holds
H is StableSubgroup of H
let H1 be strict StableSubgroup of G; :: thesis: ( A c= the carrier of H1 implies H is StableSubgroup of H1 )
A22: the carrier of H1 = carr H1 ;
assume A c= the carrier of H1 ; :: thesis: H is StableSubgroup of H1
then the carrier of H1 in X by A1, A22;
hence H is StableSubgroup of H1 by A21, Lm20, SETFAM_1:3; :: thesis: verum