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