theorem :: GRCAT_1:39

for UN being Universe holds the carrier of (MidOpGroupCat UN) = MidOpGroupObjects UN ;