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 )
A1: x + 0 < z by XREAL_1:10, XXREAL_0:25;
y + 0 < z by XREAL_1:10, XXREAL_0:25;
hence ( x < z & y < z ) by A1; :: thesis: verum