theorem :: CLASSES4:65

for UN being non trivial Universe holds REAL * in UN