theorem :: GROUP_7:15
for G1 being commutative Group holds <*G1*> is Group-like associative commutative multMagma-Family of {1} ;