let x, y be ExtReal; :: thesis: ( x <= y iff - y <= - x )
thus ( x <= y implies - y <= - x ) by Lm15; :: thesis: ( - y <= - x implies x <= y )
( - y <= - x implies - (- x) <= - (- y) ) by Lm15;
hence ( - y <= - x implies x <= y ) ; :: thesis: verum