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 ) )
assume A1: ( a < b & a < c ) ; :: thesis: ex x being R_eal st
( a < x & x < b & x < c & x in REAL )
X: min b,c = min {b,c} by XXREAL_2:14;
reconsider m = min b,c as R_eal by XXREAL_0:def 1;
a < min b,c by A1, XXREAL_0:def 9;
then consider x being R_eal such that
A2: ( a < x & x < m & x in REAL ) by Th17;
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 A3: min b,c <= b by X, XXREAL_2:62;
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 A4: min b,c <= c by X, XXREAL_2:62;
take x ; :: thesis: ( a < x & x < b & x < c & x in REAL )
thus ( a < x & x < b & x < c & x in REAL ) by A2, A3, A4, XXREAL_0:2; :: thesis: verum