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 )

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 )

hence ( a < x & x < b & x < c & x in REAL ) by A3, A2, XXREAL_0:2; :: thesis: verum

( 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

then A2:
min (b,c) <= c
by A1, XXREAL_2:62;
take
c
; :: thesis: ( c in {b,c} & c <= c )

thus ( c in {b,c} & c <= c ) by TARSKI:def 2; :: thesis: verum

end;thus ( c in {b,c} & c <= c ) by TARSKI:def 2; :: thesis: verum

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

then
min (b,c) <= b
by A1, XXREAL_2:62;
take
b
; :: thesis: ( b in {b,c} & b <= b )

thus ( b in {b,c} & b <= b ) by TARSKI:def 2; :: thesis: verum

end;thus ( b in {b,c} & b <= b ) by TARSKI:def 2; :: thesis: verum

hence ( a < x & x < b & x < c & x in REAL ) by A3, A2, XXREAL_0:2; :: thesis: verum