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 A1: 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 )
for r, p being real number st r in X & p in Y holds
r <= p by A1;
then consider g being real number such that
A2: for r, p being real number st r in X & p in Y holds
( r <= g & g <= p ) by AXIOMS:26;
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 A2; :: thesis: verum