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