let x, y be R_eal; :: thesis: ( x <= y implies y - x >= 0 )
assume Z: x <= y ; :: thesis: y - x >= 0

per cases ( ( - x in REAL & y in REAL ) or ( - x = +infty & y <> -infty ) or ( y = +infty & - x <> -infty ) or ( - x = -infty & y <> +infty ) or ( y = -infty & - x <> +infty ) or ( ( not - x in REAL or not y in REAL ) & not ( - x = +infty & y <> -infty ) & not ( y = +infty & - x <> -infty ) & not ( - x = -infty & y <> +infty ) & not ( y = -infty & - x <> +infty ) ) ) ;

suppose S: ( - x in REAL & y in REAL ) ; :: thesis: y - x >= 0

then consider a, b being Real such that
W1: - x = a and
W2: y = b and
W3: y - x = a + b by Def2;
ex a being Real st
( - x = a & - (- x) = - a ) by Def3, S;
then b - (- a) >= 0 by W2, Z, W1, XREAL_1:50;
hence y - x >= 0 by W3; :: thesis: verum

end;

suppose ( ( - x = +infty & y <> -infty ) or ( y = +infty & - x <> -infty ) ) ; :: thesis: y - x >= 0

then y - x = +infty by Def2;
hence y - x >= 0 by XXREAL_0:3; :: thesis: verum

end;

suppose ( - x = -infty & y <> +infty ) ; :: thesis: y - x >= 0

hence y - x >= 0 by Z, Th4, XXREAL_0:4; :: thesis: verum

end;

suppose ( y = -infty & - x <> +infty ) ; :: thesis: y - x >= 0

hence y - x >= 0 by Th4, Z, XXREAL_0:6; :: thesis: verum

end;

suppose ( ( not - x in REAL or not y in REAL ) & not ( - x = +infty & y <> -infty ) & not ( y = +infty & - x <> -infty ) & not ( - x = -infty & y <> +infty ) & not ( y = -infty & - x <> +infty ) ) ; :: thesis: y - x >= 0

hence y - x >= 0 by Def2; :: thesis: verum

end;

end;