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 )

G is commutative by STRUCT_0:def 5, A2, Th77;

hence G is commutative Group ; :: thesis: verum

thus ( G is commutative Group implies center G = G ) :: thesis: ( center G = G implies G is commutative Group )

proof

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

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

hence
center G = G
by GROUP_2:62; :: thesis: verumlet 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;for b being Element of G holds a * b = b * a by A1, Lm1;

hence a in center G by Th77; :: thesis: verum

G is commutative by STRUCT_0:def 5, A2, Th77;

hence G is commutative Group ; :: thesis: verum