for X, Y being real-membered set st X <> {} & Y <> {} & ( for a, b being Real st a in X & b in Y holds
a <= b ) holds
ex d being Real st
( ( for a being Real st a in X holds
a <= d ) & ( for b being Real st b in Y holds
d <= b ) )