let x, y be Surreal; :: thesis: ( x == y & x is *real implies y is *real )
assume A1: ( x == y & x is *real ) ; :: thesis: y is *real
then consider n being Nat such that
A2: ( uInt . (- n) < x & x < uInt . n ) ;
A3: ( uInt . (- n) < y & y < uInt . n ) by A2, A1, SURREALO:4;
( x == real_qua x & real_qua x == real_qua y ) by A1, Lm20;
then x == real_qua y by SURREALO:4;
then y == real_qua y by A1, SURREALO:4;
hence y is *real by A3; :: thesis: verum