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