:: deftheorem defines 1: GROUP_6:def 7 :
for G, H being non empty multMagma holds 1: (G,H) = G --> (1_ H);