set X = { h where h is Element of G : A |^ h = A } ;
{ h where h is Element of G : A |^ h = A } c= the carrier of G
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { h where h is Element of G : A |^ h = A } or x in the carrier of G )
assume x in { h where h is Element of G : A |^ h = A } ; :: thesis: x in the carrier of G
then ex h being Element of G st
( x = h & A |^ h = A ) ;
hence x in the carrier of G ; :: thesis: verum
end;
then reconsider X = { h where h is Element of G : A |^ h = A } as Subset of G ;
A1: now :: thesis: for a, b being Element of G st a in X & b in X holds
a * b in X
let a, b be Element of G; :: thesis: ( a in X & b in X implies a * b in X )
assume ( a in X & b in X ) ; :: thesis: a * b in X
then ( ex g being Element of G st
( a = g & A |^ g = A ) & ex h being Element of G st
( b = h & A |^ h = A ) ) ;
then A |^ (a * b) = A by Th47;
hence a * b in X ; :: thesis: verum
end;
A2: now :: thesis: for a being Element of G st a in X holds
a " in X
let a be Element of G; :: thesis: ( a in X implies a " in X )
assume a in X ; :: thesis: a " in X
then ex b being Element of G st
( a = b & A |^ b = A ) ;
then A = A |^ (a ") by Th54;
hence a " in X ; :: thesis: verum
end;
A |^ (1_ G) = A by Th52;
then 1_ G in X ;
hence ex b1 being strict Subgroup of G st the carrier of b1 = { h where h is Element of G : A |^ h = A } by A1, A2, GROUP_2:52; :: thesis: verum