:: deftheorem Def15 defines Group_DOMAIN-like GRCAT_1:def 17 :
for IT being set holds
( IT is Group_DOMAIN-like iff for x being object st x in IT holds
x is strict AddGroup );