let G be strict Group; :: thesis: ( G is commutative Group iff center G = G )
thus ( G is commutative Group implies center G = G ) :: thesis: ( center G = G implies G is commutative Group )

proof

assume A1: G is commutative Group ; :: thesis: center G = G

now :: thesis: for a being Element of G holds a in center G

let a be Element of G; :: thesis: a in center G
for b being Element of G holds a * b = b * a by A1, Lm1;
hence a in center G by Th77; :: thesis: verum

end;

hence center G = G by GROUP_2:62; :: thesis: verum

end;

assume A2: center G = G ; :: thesis: G is commutative Group
G is commutative by STRUCT_0:def 5, A2, Th77;
hence G is commutative Group ; :: thesis: verum