defpred S₁[ 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 & S₁[Y] ) ) from XBOOLE_0: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

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in meet X or y in the carrier of G )
consider x being set such that
A6: x in X by A4;
consider H being strict StableSubgroup of G such that
A7: x = carr H and
A c= x by A1, A6;
assume y in meet X ; :: thesis: y in the carrier of G
then y in carr H by A6, A7, SETFAM_1:def 1;
hence y in the carrier of G ; :: thesis: verum

end;

now

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
A8: Y = carr H and
A c= Y by A1;
1_ G in H by Lm18;
hence 1_ G in Y by A8, STRUCT_0:def 5; :: thesis: verum

end;

then A9: meet X <> {} by A3, SETFAM_1:def 1;
reconsider M = meet X as Subset of G by A5;

A10: now

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 A11: a in M ; :: thesis: (G ^ o) . a in M

now

let Y be set ; :: thesis: ( Y in X implies (G ^ o) . a in Y )
assume A12: Y in X ; :: thesis: (G ^ o) . a in Y
then consider H being strict StableSubgroup of G such that
A13: Y = carr H and
A c= Y by A1;
a in carr H by A11, A12, A13, SETFAM_1:def 1;
then a in H by STRUCT_0:def 5;
then (G ^ o) . a in H by Lm10;
hence (G ^ o) . a in Y by A13, STRUCT_0:def 5; :: thesis: verum

end;

hence (G ^ o) . a in M by A3, SETFAM_1:def 1; :: thesis: verum

end;

A14: now

let a, b be Element of G; :: thesis: ( a in M & b in M implies a * b in M )
assume that
A15: a in M and
A16: b in M ; :: thesis: a * b in M

now

let Y be set ; :: thesis: ( Y in X implies a * b in Y )
assume A17: Y in X ; :: thesis: a * b in Y
then consider H being strict StableSubgroup of G such that
A18: Y = carr H and
A c= Y by A1;
b in carr H by A16, A17, A18, SETFAM_1:def 1;
then A19: b in H by STRUCT_0:def 5;
a in carr H by A15, A17, A18, SETFAM_1:def 1;
then a in H by STRUCT_0:def 5;
then a * b in H by A19, Lm19;
hence a * b in Y by A18, STRUCT_0:def 5; :: thesis: verum

end;

hence a * b in M by A3, SETFAM_1:def 1; :: thesis: verum

end;

now

let a be Element of G; :: thesis: ( a in M implies a " in M )
assume A20: a in M ; :: thesis: a " in M

now

let Y be set ; :: thesis: ( Y in X implies a " in Y )
assume A21: Y in X ; :: thesis: a " in Y
then consider H being strict StableSubgroup of G such that
A22: Y = carr H and
A c= Y by A1;
a in carr H by A20, A21, A22, SETFAM_1:def 1;
then a in H by STRUCT_0:def 5;
then a " in H by Lm20;
hence a " in Y by A22, 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
A23: the carrier of H = M by A9, A14, A10, Lm15;
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

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, A23, 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 )
A24: 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, A24;
hence H is StableSubgroup of H1 by A23, Lm21, SETFAM_1:3; :: thesis: verum