theorem :: CLASSES4:66

for UN being non trivial Universe holds ExtREAL * in UN