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