let UN be Universe; :: thesis: Trivial-addLoopStr in MidOpGroupObjects UN
Trivial-addLoopStr in the carrier of (AbGroupCat UN) by Th36;
hence Trivial-addLoopStr in MidOpGroupObjects UN ; :: thesis: verum