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 ) ) )
assume A1: ( 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 ) ) )
assume A2: 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 ) )
consider x being Element of X;
reconsider a = x as real number by A1, TARSKI:def 3;
A3: a in X by A1;
consider y being Element of Y;
reconsider b = y as real number by A1, TARSKI:def 3;
A4: b in Y by A1;
( X c= REAL & Y c= REAL ) by Th3;
then consider d being real number such that
A5: 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 by XREAL_0:def 1;
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 A3, A4, A5; :: thesis: verum