theorem Th49: :: XXREAL_3:49

for x, z being ExtReal st 0 <= x & x < z holds
ex y being Real st
( 0 < y & x + y < z )