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

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 Th89; :: 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

proof

let a, b be Element of G; :: according to GROUP_1:def 12 :: thesis: a * b = b * a
a in G by STRUCT_0:def 5;
hence a * b = b * a by A2, Th89; :: thesis: verum

end;

hence G is commutative Group ; :: thesis: verum