then A3:
{ b where b is Element of G : a * b = b * a } is Subset of G
byTARSKI: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 }