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 ) )
assume A1: ( a < c & b < c ) ; :: thesis: ex x being R_eal st
( a < x & b < x & x < c & x in REAL )
X: max a,b = max {a,b} by XXREAL_2:12;
reconsider m = max a,b as R_eal by XXREAL_0:def 1;
max a,b < c by A1, XXREAL_0:def 10;
then consider x being R_eal such that
A2: ( m < x & x < c & x in REAL ) by Th17;
take x ; :: thesis: ( a < x & b < x & x < c & x in REAL )
( a in {a,b} & b in {a,b} ) by TARSKI:def 2;
hence ( a < x & b < x & x < c & x in REAL ) by A2, X, XXREAL_2:61; :: thesis: verum