for X, Y being Subset of REAL st ( for x, y being Real st x in X & y in Y holds
x <= y ) holds
ex z being Real st
for x, y being Real st x in X & y in Y holds
( x <= z & z <= y )