:: deftheorem defines (Omega). GROUP_9:def 9 :
for O being set
for G being GroupWithOperators of O holds (Omega). G = HGrWOpStr(# the carrier of G, the multF of G, the action of G #);