theorem Th46: :: XXREAL_3:46

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