let a, b, c be R_eal; :: thesis: ( a < b & a < c implies ex x being R_eal st
( a < x & x < b & x < c & x in REAL ) )
A1: min (b,c) = min {b,c} by XXREAL_2:14;
ex o being R_eal st
( o in {b,c} & o <= c )
proof
take c ; :: thesis: ( c in {b,c} & c <= c )
thus ( c in {b,c} & c <= c ) by TARSKI:def 2; :: thesis: verum
end;
then A2: min (b,c) <= c by A1, XXREAL_2:62;
reconsider m = min (b,c) as R_eal by XXREAL_0:def 1;
assume ( a < b & a < c ) ; :: thesis: ex x being R_eal st
( a < x & x < b & x < c & x in REAL )
then a < min (b,c) by XXREAL_0:def 9;
then consider x being R_eal such that
A3: ( a < x & x < m & x in REAL ) by Th2;
take x ; :: thesis: ( a < x & x < b & x < c & x in REAL )
ex o being R_eal st
( o in {b,c} & o <= b )
proof
take b ; :: thesis: ( b in {b,c} & b <= b )
thus ( b in {b,c} & b <= b ) by TARSKI:def 2; :: thesis: verum
end;
then min (b,c) <= b by A1, XXREAL_2:62;
hence ( a < x & x < b & x < c & x in REAL ) by A3, A2, XXREAL_0:2; :: thesis: verum