let x, y be ExtReal; :: thesis: ( x <= y implies y - x >= 0 )
assume x <= y ; :: thesis: y - x >= 0
then - y <= - x by Lm15;
then (- y) + y <= y + (- x) by Th36;
hence y - x >= 0 by Th7; :: thesis: verum