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