let a, b, c be R_eal; :: thesis: ( a < c & b < c implies ex x being R_eal st
( a < x & b < x & x < c & x in REAL ) )
reconsider m = max (a,b) as R_eal by XXREAL_0:def 1;
A1: b in {a,b} by TARSKI:def 2;
assume ( a < c & b < c ) ; :: thesis: ex x being R_eal st
( a < x & b < x & x < c & x in REAL )
then max (a,b) < c by XXREAL_0:def 10;
then consider x being R_eal such that
A2: ( m < x & x < c & x in REAL ) by Th2;
take x ; :: thesis: ( a < x & b < x & x < c & x in REAL )
( max (a,b) = max {a,b} & a in {a,b} ) by TARSKI:def 2, XXREAL_2:12;
hence ( a < x & b < x & x < c & x in REAL ) by A2, A1, XXREAL_2:61; :: thesis: verum