set Car = { b where b is Element of G : a * b = b * a } ;
( a * (1_ G) = a & (1_ G) * a = a ) by GROUP_1:def 5;
then A1: 1_ G in { b where b is Element of G : a * b = b * a } ;
for x being set st x in { b where b is Element of G : a * b = b * a } holds
x in the carrier of G

proof

let x be set ; :: thesis: ( x in { b where b is Element of G : a * b = b * a } implies x in the carrier of G )
assume A2: x in { b where b is Element of G : a * b = b * a } ; :: thesis: x in the carrier of G
consider g being Element of G such that
A3: ( x = g & a * g = g * a ) by A2;
thus x in the carrier of G by A3; :: thesis: verum

end;

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

proof

let g1, g2 be Element of G; :: thesis: ( g1 in { b where b is Element of G : a * b = b * a } & g2 in { b where b is Element of G : a * b = b * a } implies g1 * g2 in { b where b is Element of G : a * b = b * a } )
assume that
A6: g1 in { b where b is Element of G : a * b = b * a } and
A7: g2 in { b where b is Element of G : a * b = b * a } ; :: thesis: g1 * g2 in { b where b is Element of G : a * b = b * a }
consider z1 being Element of G such that
A8: ( z1 = g1 & z1 * a = a * z1 ) by A6;
consider z2 being Element of G such that
A9: ( z2 = g2 & z2 * a = a * z2 ) by A7;
a * (g1 * g2) = (g1 * a) * g2 by A8, GROUP_1:def 4
.= g1 * (g2 * a) by A9, GROUP_1:def 4
.= (g1 * g2) * a by GROUP_1:def 4 ;
hence g1 * g2 in { b where b is Element of G : a * b = b * a } ; :: thesis: verum

end;

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

proof

let g be Element of G; :: thesis: ( g in { b where b is Element of G : a * b = b * a } implies g " in { b where b is Element of G : a * b = b * a } )
assume A10: g in { b where b is Element of G : a * b = b * a } ; :: thesis: g " in { b where b is Element of G : a * b = b * a }
consider z1 being Element of G such that
A11: ( z1 = g & z1 * a = a * z1 ) by A10;
(g " ) * (g * a) = a by GROUP_3:1;
then (g " ) * ((a * g) * (g " )) = a * (g " ) by A11, GROUP_1:def 4;
then (g " ) * a = a * (g " ) by GROUP_3:1;
hence g " in { b where b is Element of G : 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 : a * b = b * a } by A1, A4, A5, GROUP_2:61; :: thesis: verum