let O be set ; :: thesis: for G being GroupWithOperators of O
for A being Subset of G holds the carrier of = meet { B where B is Subset of G : ex H being strict StableSubgroup of G st
( B = the carrier of H & A c= carr H )
}

let G be GroupWithOperators of O; :: thesis: for A being Subset of G holds the carrier of = meet { B where B is Subset of G : ex H being strict StableSubgroup of G st
( B = the carrier of H & A c= carr H )
}

let A be Subset of G; :: thesis: the carrier of = meet { B where B is Subset of G : ex H being strict StableSubgroup of G st
( B = the carrier of H & A c= carr H )
}

defpred S1[ StableSubgroup of G] means A c= carr \$1;
set X = { B where B is Subset of G : ex H being strict StableSubgroup of G st
( B = the carrier of H & A c= carr H )
}
;
A1: now :: thesis: for Y being set st Y in { B where B is Subset of G : ex H being strict StableSubgroup of G st
( B = the carrier of H & A c= carr H )
}
holds
A c= Y
let Y be set ; :: thesis: ( Y in { B where B is Subset of G : ex H being strict StableSubgroup of G st
( B = the carrier of H & A c= carr H )
}
implies A c= Y )

assume Y in { B where B is Subset of G : ex H being strict StableSubgroup of G st
( B = the carrier of H & A c= carr H )
}
; :: thesis: A c= Y
then ex B being Subset of G st
( Y = B & ex H being strict StableSubgroup of G st
( B = the carrier of H & A c= carr H ) ) ;
hence A c= Y ; :: thesis: verum
end;
the carrier of () = carr () ;
then A2: ex H being strict StableSubgroup of G st S1[H] ;
consider H being strict StableSubgroup of G such that
A3: the carrier of H = meet { B where B is Subset of G : ex H being strict StableSubgroup of G st
( B = the carrier of H & S1[H] )
}
from
A4: now :: thesis: for H1 being strict StableSubgroup of G st A c= the carrier of H1 holds
H is StableSubgroup of H1
let H1 be strict StableSubgroup of G; :: thesis: ( A c= the carrier of H1 implies H is StableSubgroup of H1 )
A5: 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 { B where B is Subset of G : ex H being strict StableSubgroup of G st
( B = the carrier of H & A c= carr H )
}
by A5;
hence H is StableSubgroup of H1 by ; :: thesis: verum
end;
carr () in { B where B is Subset of G : ex H being strict StableSubgroup of G st
( B = the carrier of H & A c= carr H )
}
;
then A c= the carrier of H by ;
hence the carrier of = meet { B where B is Subset of G : ex H being strict StableSubgroup of G st
( B = the carrier of H & A c= carr H )
}
by ; :: thesis: verum