let x, y be Surreal; :: thesis: ( x == y implies real_qua x <= real_qua y )
assume A1: x == y ; :: thesis: real_qua x <= real_qua y
A2: L_ (real_qua x) << {(real_qua y)}

proof

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not l in L_ (real_qua x) or not r in {(real_qua y)} or not r <= l )
assume A3: ( l in L_ (real_qua x) & r in {(real_qua y)} ) ; :: thesis: not r <= l
then l in { (x - ((uInt . n) ")) where n is positive Nat : verum } by Def8;
then consider nL being positive Nat such that
A4: l = x - ((uInt . nL) ") ;
1 * nL < 2 * nL by XREAL_1:68;
then ( uReal . (1 / (2 * nL)) < uReal . (1 / nL) & uReal . (1 / nL) == (uInt . nL) " ) by XREAL_1:76, Th58, Th51;
then ( (uInt . (2 * nL)) " == uReal . (1 / (2 * nL)) & uReal . (1 / (2 * nL)) < (uInt . nL) " ) by Th58, SURREALO:4;
then (uInt . (2 * nL)) " < (uInt . nL) " by SURREALO:4;
then - ((uInt . nL) ") < - ((uInt . (2 * nL)) ") by SURREALR:10;
then A5: x + (- ((uInt . nL) ")) <= y + (- ((uInt . (2 * nL)) ")) by A1, SURREALR:44;
r = real_qua y by A3, TARSKI:def 1;
then y - ((uInt . (2 * nL)) ") < r by Th59;
hence not r <= l by A4, A5, SURREALO:4; :: thesis: verum

end;

{(real_qua x)} << R_ (real_qua y)

proof

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not l in {(real_qua x)} or not r in R_ (real_qua y) or not r <= l )
assume A6: ( l in {(real_qua x)} & r in R_ (real_qua y) ) ; :: thesis: not r <= l
then r in { (y + ((uInt . n) ")) where n is positive Nat : verum } by Def8;
then consider nL being positive Nat such that
A7: r = y + ((uInt . nL) ") ;
1 * nL < 2 * nL by XREAL_1:68;
then ( uReal . (1 / (2 * nL)) < uReal . (1 / nL) & uReal . (1 / nL) == (uInt . nL) " ) by XREAL_1:76, Th58, Th51;
then ( (uInt . (2 * nL)) " == uReal . (1 / (2 * nL)) & uReal . (1 / (2 * nL)) < (uInt . nL) " ) by Th58, SURREALO:4;
then (uInt . (2 * nL)) " < (uInt . nL) " by SURREALO:4;
then A8: x + ((uInt . (2 * nL)) ") <= y + ((uInt . nL) ") by A1, SURREALR:44;
l = real_qua x by A6, TARSKI:def 1;
hence not r <= l by A7, A8, Th59, SURREALO:4; :: thesis: verum

end;

hence real_qua x <= real_qua y by A2, SURREAL0:43; :: thesis: verum