theorem Th1: :: CHAIN_1:1

for x, y being Real st x < y holds
ex z being Element of REAL st
( x < z & z < y )