theorem Th54: :: CLASSES4:54

for UN being non trivial Universe holds ExtREAL is Element of UN