theorem :: GROUP_5:75

for G being strict Group holds
( G is commutative Group iff G ` = (1). G )