let x, y be Real; :: thesis: ex z being Element of REAL st

( x < z & y < z )

reconsider x = x, y = y as Real ;

reconsider z = (max (x,y)) + 1 as Element of REAL by XREAL_0:def 1;

take z ; :: thesis: ( x < z & y < z )

A1: x + 0 < z by XREAL_1:8, XXREAL_0:25;

y + 0 < z by XREAL_1:8, XXREAL_0:25;

hence ( x < z & y < z ) by A1; :: thesis: verum

( x < z & y < z )

reconsider x = x, y = y as Real ;

reconsider z = (max (x,y)) + 1 as Element of REAL by XREAL_0:def 1;

take z ; :: thesis: ( x < z & y < z )

A1: x + 0 < z by XREAL_1:8, XXREAL_0:25;

y + 0 < z by XREAL_1:8, XXREAL_0:25;

hence ( x < z & y < z ) by A1; :: thesis: verum