theorem :: CLASSES5:79

for U being Universe holds union { the carrier of (Trivial-addLoopStr x) where x is Element of U : verum } = U