let x, y be real number ; :: thesis: ex z being Real st
( x < z & y < z )
reconsider x = x, y = y as Real by XREAL_0:def 1;
take z = (max x,y) + 1; :: thesis: ( x < z & y < z )
( x + 0 < z & y + 0 < z ) by XREAL_1:10, XXREAL_0:25;
hence ( x < z & y < z ) ; :: thesis: verum