let X, Y be Subset of REAL; :: thesis: ( ( for r, p being Real st r in X & p in Y holds
r < p ) implies ex g being Real st
for r, p being Real st r in X & p in Y holds
( r <= g & g <= p ) )
assume for r, p being Real st r in X & p in Y holds
r < p ; :: thesis: ex g being Real st
for r, p being Real st r in X & p in Y holds
( r <= g & g <= p )
then for r, p being Real st r in X & p in Y holds
r <= p ;
then consider g being Real such that
A1: for r, p being Real st r in X & p in Y holds
( r <= g & g <= p ) by AXIOMS:1;
reconsider g = g as Real ;
take g ; :: thesis: for r, p being Real st r in X & p in Y holds
( r <= g & g <= p )
thus for r, p being Real st r in X & p in Y holds
( r <= g & g <= p ) by A1; :: thesis: verum