:: deftheorem defines AbGroupCat GRCAT_1:def 32 :
for UN being Universe holds AbGroupCat UN = cat (AbGroupObjects UN);