set Car = { b where b is Element of G : a * b = b * a } ;
A1: a * (1_ G) = a by GROUP_1:def 4;
(1_ G) * a = a by GROUP_1:def 4;
then A2: 1_ G in { b where b is Element of G : a * b = b * a } by A1;
for x being object 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 object ; :: thesis: ( x in { b where b is Element of G : a * b = b * a } implies x in the carrier of G )
assume x in { b where b is Element of G : a * b = b * a } ; :: thesis: x in the carrier of G
then ex g being Element of G st
( x = g & a * g = g * a ) ;
hence x in the carrier of G ; :: thesis: verum

end;

then A3: { b where b is Element of G : a * b = b * a } is Subset of G by TARSKI:def 3;
A4: 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
A5: g1 in { b where b is Element of G : a * b = b * a } and
A6: 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 }
A7: ex z1 being Element of G st
( z1 = g1 & z1 * a = a * z1 ) by A5;
A8: ex z2 being Element of G st
( z2 = g2 & z2 * a = a * z2 ) by A6;
a * (g1 * g2) = (g1 * a) * g2 by A7, GROUP_1:def 3
.= g1 * (g2 * a) by A8, GROUP_1:def 3
.= (g1 * g2) * a by GROUP_1:def 3 ;
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 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 }
then A9: ex z1 being Element of G st
( z1 = g & z1 * a = a * z1 ) ;
(g ") * (g * a) = a by GROUP_3:1;
then (g ") * ((a * g) * (g ")) = a * (g ") by A9, GROUP_1:def 3;
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 A2, A3, A4, GROUP_2:52; :: thesis: verum