let G be Group; :: thesis: center G is commutative
let a, b be Element of (center G); :: according to GROUP_1:def 12 :: thesis: a * b = b * a
reconsider x = a, y = b as Element of G by GROUP_2:42;
A1: a in center G by STRUCT_0:def 5;
thus a * b = x * y by GROUP_2:43
.= y * x by A1, Th77
.= b * a by GROUP_2:43 ; :: thesis: verum