theorem Th62: :: SURREALN:62

for x being Surreal holds
( x is *real iff ex r being Real st x == uReal . r )