let x be Surreal; :: thesis: for n being positive Nat holds
( x - ((uInt . n) ") < real_qua x & real_qua x < x + ((uInt . n) ") )
let n be positive Nat; :: thesis: ( x - ((uInt . n) ") < real_qua x & real_qua x < x + ((uInt . n) ") )
x - ((uInt . n) ") in { (x - ((uInt . k) ")) where k is positive Nat : verum } ;
then A1: x + (- ((uInt . n) ")) in L_ (real_qua x) by Def8;
x + ((uInt . n) ") in { (x + ((uInt . k) ")) where k is positive Nat : verum } ;
then A2: x + ((uInt . n) ") in R_ (real_qua x) by Def8;
( L_ (real_qua x) << {(real_qua x)} & {(real_qua x)} << R_ (real_qua x) & real_qua x in {(real_qua x)} ) by TARSKI:def 1, SURREALO:11;
hence ( x - ((uInt . n) ") < real_qua x & real_qua x < x + ((uInt . n) ") ) by A1, A2; :: thesis: verum