theorem :: GRCAT_1:40

for UN being Universe holds Trivial-addLoopStr in MidOpGroupObjects UN