theorem Th25: :: XREAL_1:25

for a, b being Real st a <= - b holds
b <= - a