:: deftheorem defines MidOpGroupObjects GRCAT_1:def 33 :
for UN being Universe holds MidOpGroupObjects UN = { G where G is Element of (AbGroupCat UN) : ex H being midpoint_operator AbGroup st G = H } ;