theorem Th79: :: CLASSES5:77

for U being Universe
for x being Element of U holds comp (Trivial-addLoopStr x) is Element of U