set Car = { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a } ;
C1: 1_ G in { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a }

proof

for a being Element of G st a in A holds
(1_ G) * a = a * (1_ G)

proof

let a be Element of G; :: thesis: ( a in A implies (1_ G) * a = a * (1_ G) )
assume a in A ; :: thesis: (1_ G) * a = a * (1_ G)
(1_ G) * a = a by GROUP_1:def 4
.= a * (1_ G) by GROUP_1:def 4 ;
hence (1_ G) * a = a * (1_ G) ; :: thesis: verum

end;

hence 1_ G in { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a } ; :: thesis: verum

end;

for x being object st x in { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a } holds
x in the carrier of G

proof

let x be object ; :: thesis: ( x in { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a } implies x in the carrier of G )
assume x in { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a } ; :: thesis: x in the carrier of G
then ex g being Element of G st
( x = g & ( for a being Element of G st a in A holds
a * g = g * a ) ) ;
hence x in the carrier of G ; :: thesis: verum

end;

then C2: { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a } is Subset of G by TARSKI:def 3;
C3: for g1, g2 being Element of G st g1 in { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a } & g2 in { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a } holds
g1 * g2 in { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a }

proof

let g1, g2 be Element of G; :: thesis: ( g1 in { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a } & g2 in { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a } implies g1 * g2 in { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a } )
assume B1: g1 in { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a } ; :: thesis: ( not g2 in { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a } or g1 * g2 in { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a } )
assume B2: g2 in { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a } ; :: thesis: g1 * g2 in { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a }
B3: ex z1 being Element of G st
( z1 = g1 & ( for a being Element of G st a in A holds
a * z1 = z1 * a ) ) by B1;
B4: ex z2 being Element of G st
( z2 = g2 & ( for a being Element of G st a in A holds
a * z2 = z2 * a ) ) by B2;
for a being Element of G st a in A holds
a * (g1 * g2) = (g1 * g2) * a

proof

let a be Element of G; :: thesis: ( a in A implies a * (g1 * g2) = (g1 * g2) * a )
assume Z1: a in A ; :: thesis: a * (g1 * g2) = (g1 * g2) * a
a * (g1 * g2) = (a * g1) * g2 by GROUP_1:def 3
.= (g1 * a) * g2 by Z1, B3
.= g1 * (a * g2) by GROUP_1:def 3
.= g1 * (g2 * a) by Z1, B4
.= (g1 * g2) * a by GROUP_1:def 3 ;
hence a * (g1 * g2) = (g1 * g2) * a ; :: thesis: verum

end;

hence g1 * g2 in { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a } ; :: thesis: verum

end;

for g being Element of G st g in { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a } holds
g " in { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a }

proof

let g be Element of G; :: thesis: ( g in { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a } implies g " in { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a } )
assume g in { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a } ; :: thesis: g " in { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a }
then Z1: ex z1 being Element of G st
( z1 = g & ( for a being Element of G st a in A holds
z1 * a = a * z1 ) ) ;
for a being Element of G st a in A holds
(g ") * a = a * (g ")

proof

let a be Element of G; :: thesis: ( a in A implies (g ") * a = a * (g ") )
assume a in A ; :: thesis: (g ") * a = a * (g ")
then (g ") * ((a * g) * (g ")) = (g ") * ((g * a) * (g ")) by Z1
.= ((g ") * (g * a)) * (g ") by GROUP_1:def 3
.= (((g ") * g) * a) * (g ") by GROUP_1:def 3
.= ((1_ G) * a) * (g ") by GROUP_1:def 5
.= a * (g ") by GROUP_1:def 4 ;
hence (g ") * a = a * (g ") by GROUP_3:1; :: thesis: verum

end;

hence g " in { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a } ; :: thesis: verum

end;

hence ex b₁ being strict Subgroup of G st the carrier of b₁ = { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a } by C1, C2, C3, GROUP_2:52; :: thesis: verum