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