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 set M = meet X;
A2: carr () = the carrier of () ;
then A3: X <> {} by A1;
A4: the carrier of G in X by A1, A2;
A5: meet X c= the carrier of G by ;
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 ; :: thesis: verum
end;
then A7: meet X <> {} by ;
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 ;
then a in H by STRUCT_0:def 5;
then (G ^ o) . a in H by Lm9;
hence (G ^ o) . a in Y by ; :: thesis: verum
end;
hence (G ^ o) . a in M by ; :: 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 ;
then A17: b in H by STRUCT_0:def 5;
a in carr H by ;
then a in H by STRUCT_0:def 5;
then a * b in H by ;
hence a * b in Y by ; :: thesis: verum
end;
hence a * b in M by ; :: 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 ;
then a in H by STRUCT_0:def 5;
then a " in H by Lm19;
hence a " in Y by ; :: thesis: verum
end;
hence a " in M by ; :: 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 ; :: 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 ;
hence H is StableSubgroup of H1 by ; :: thesis: verum