let x, y be ExtReal; :: thesis: ( ( x <= - y implies y <= - x ) & ( - x <= y implies - y <= x ) )
( x <= - y implies - (- y) <= - x ) by Th38;
hence ( x <= - y implies y <= - x ) ; :: thesis: ( - x <= y implies - y <= x )
( - x <= y implies - y <= - (- x) ) by Th38;
hence ( - x <= y implies - y <= x ) ; :: thesis: verum