theorem :: XXREAL_3:60

for x, y being ExtReal holds
( ( x <= - y implies y <= - x ) & ( - x <= y implies - y <= x ) )