theorem :: GRCAT_1:38

for UN being Universe holds the carrier of (AbGroupCat UN) = AbGroupObjects UN ;