theorem Th51: :: XXREAL_3:51

for x, y being ExtReal st x < y & x < +infty & -infty < y holds
0 < y - x