:: deftheorem defines MidOpGroupCat GRCAT_1:def 34 :
for UN being Universe holds MidOpGroupCat UN = cat (MidOpGroupObjects UN);