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

( 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