:: deftheorem defines *real SURREALN:def 9 :
for x being Surreal holds
( x is *real iff ( x == real_qua x & ex n being Nat st
( uInt . (- n) < x & x < uInt . n ) ) );