let G be Group; :: thesis: center G is normal Subgroup of G

now :: thesis: for a being Element of G holds a * (center G) c= (center G) * a

let a be Element of G; :: thesis: a * (center G) c= (center G) * a
thus a * (center G) c= (center G) * a :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in a * (center G) or x in (center G) * a )
assume x in a * (center G) ; :: thesis: x in (center G) * a
then consider b being Element of G such that
A1: x = a * b and
A2: b in center G by GROUP_2:103;
x = b * a by A1, A2, Th77;
hence x in (center G) * a by A2, GROUP_2:104; :: thesis: verum

end;

end;

hence center G is normal Subgroup of G by GROUP_3:118; :: thesis: verum