:: deftheorem defines AbGroupObjects GRCAT_1:def 31 :
for UN being Universe holds AbGroupObjects UN = { G where G is Element of (GroupCat UN) : ex H being AbGroup st G = H } ;