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 * (0_ G) = A by ThB52;
then 0_ 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, Th52; :: thesis: verum