theorem Th3: :: XXREAL_3:3

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