theorem Th80: :: CLASSES5:78

for U being Universe
for x being Element of U ex y being Element of U st GO y, Trivial-addLoopStr x