let X, Y be real-membered set ; :: thesis: ( X <> {} & Y <> {} & ( for a, b being Real st a in X & b in Y holds
a <= b ) implies 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 ) ) )
set x = the Element of X;
reconsider a = the Element of X as Real ;
set y = the Element of Y;
reconsider b = the Element of Y as Real ;
assume ( X <> {} & Y <> {} ) ; :: thesis: ( ex a, b being Real st
( a in X & b in Y & not a <= b ) or 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 ) ) )
then A1: ( a in X & b in Y ) ;
A2: ( X c= REAL & Y c= REAL ) by Th3;
assume for a, b being Real st a in X & b in Y holds
a <= b ; :: thesis: 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 ) )
then consider d being Real such that
A3: for a, b being Real st a in X & b in Y holds
( a <= d & d <= b ) by A2, AXIOMS:1;
reconsider d = d as Real ;
take d ; :: thesis: ( ( for a being Real st a in X holds
a <= d ) & ( for b being Real st b in Y holds
d <= b ) )
thus ( ( for a being Real st a in X holds
a <= d ) & ( for b being Real st b in Y holds
d <= b ) ) by A1, A3; :: thesis: verum