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