theorem :: XREAL_1:24

for a, b being Real holds
( a <= b iff - b <= - a ) by Lm14, Lm15;