theorem :: CLASSES4:67

for UN being non trivial Universe holds COMPLEX * in UN by Th64, Th55;