defpred S1[ object , object ] means ex H being strict StableSubgroup of G st
( \$2 = H & \$1 = the carrier of H );
defpred S2[ set ] means ex H being strict StableSubgroup of G st \$1 = the carrier of H;
consider B being set such that
A1: for x being set holds
( x in B iff ( x in bool the carrier of G & S2[x] ) ) from A2: for x, y1, y2 being object st S1[x,y1] & S1[x,y2] holds
y1 = y2 by Lm4;
consider f being Function such that
A3: for x, y being object holds
( [x,y] in f iff ( x in B & S1[x,y] ) ) from for x being object holds
( x in B iff ex y being object st [x,y] in f )
proof
let x be object ; :: thesis: ( x in B iff ex y being object st [x,y] in f )
thus ( x in B implies ex y being object st [x,y] in f ) :: thesis: ( ex y being object st [x,y] in f implies x in B )
proof
assume A4: x in B ; :: thesis: ex y being object st [x,y] in f
then consider H being strict StableSubgroup of G such that
A5: x = the carrier of H by A1;
reconsider y = H as object ;
take y ; :: thesis: [x,y] in f
thus [x,y] in f by A3, A4, A5; :: thesis: verum
end;
given y being object such that A6: [x,y] in f ; :: thesis: x in B
thus x in B by A3, A6; :: thesis: verum
end;
then A7: B = dom f by XTUPLE_0:def 12;
for y being object holds
( y in rng f iff y is strict StableSubgroup of G )
proof
let y be object ; :: thesis: ( y in rng f iff y is strict StableSubgroup of G )
thus ( y in rng f implies y is strict StableSubgroup of G ) :: thesis: ( y is strict StableSubgroup of G implies y in rng f )
proof
assume y in rng f ; :: thesis: y is strict StableSubgroup of G
then consider x being object such that
A8: ( x in dom f & y = f . x ) by FUNCT_1:def 3;
[x,y] in f by ;
then ex H being strict StableSubgroup of G st
( y = H & x = the carrier of H ) by A3;
hence y is strict StableSubgroup of G ; :: thesis: verum
end;
assume y is strict StableSubgroup of G ; :: thesis: y in rng f
then reconsider H = y as strict StableSubgroup of G ;
reconsider x = the carrier of H as set ;
A9: y is set by TARSKI:1;
H is Subgroup of G by Def7;
then the carrier of H c= the carrier of G by GROUP_2:def 5;
then A10: x in dom f by A1, A7;
then [x,y] in f by A3, A7;
then y = f . x by ;
hence y in rng f by ; :: thesis: verum
end;
hence ex b1 being set st
for x being object holds
( x in b1 iff x is strict StableSubgroup of G ) ; :: thesis: verum