theorem Th1: :: SEQ_4:1

for X, Y being Subset of REAL st ( for r, p being Real st r in X & p in Y holds
r < p ) holds
ex g being Real st
for r, p being Real st r in X & p in Y holds
( r <= g & g <= p )