let x, y be ext-real number ; :: thesis: ( x <= y implies y - x >= 0 )
assume x <= y ; :: thesis: y - x >= 0
then - y <= - x by Lm3;
then (- y) + y <= y + (- x) by Th36;
hence y - x >= 0 by Tx4; :: thesis: verum