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