let U be Universe; :: thesis: for x being Element of U holds Trivial-addLoopStr x in GroupObjects U
let x be Element of U; :: thesis: Trivial-addLoopStr x in GroupObjects U
ex y being Element of U st GO y, Trivial-addLoopStr x by Th80;
hence Trivial-addLoopStr x in GroupObjects U by GRCAT_1:def 24; :: thesis: verum