theorem Th21: :: XXREAL_3:21

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