let UN be Universe; :: thesis: Trivial-addLoopStr in GroupObjects UN
ex x being set st
( x in UN & GO x, Trivial-addLoopStr ) by Th41;
hence Trivial-addLoopStr in GroupObjects UN by Def29; :: thesis: verum