let UN be Universe; :: thesis: Trivial-addLoopStr in AbGroupObjects UN
Trivial-addLoopStr in the carrier of (GroupCat UN) by Th29;
hence Trivial-addLoopStr in AbGroupObjects UN ; :: thesis: verum