theorem Th18: :: XXREAL_3:18

for x, y being ExtReal holds
( not x - y = +infty or x = +infty or y = -infty )