theorem Th2: :: CHAIN_1:2

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