let x, y be Real; :: thesis: ( 0 <= x & 0 <= y implies max (x,y) <= x + y )
assume that
A1: 0 <= x and
A2: 0 <= y ; :: thesis: max (x,y) <= x + y

now :: thesis: max (x,y) <= x + y

per cases ( max (x,y) = x or max (x,y) = y ) by XXREAL_0:16;

suppose A3: max (x,y) = x ; :: thesis: max (x,y) <= x + y

x + 0 <= x + y by A2, XREAL_1:7;
hence max (x,y) <= x + y by A3; :: thesis: verum

end;

suppose A4: max (x,y) = y ; :: thesis: max (x,y) <= x + y

y + 0 <= y + x by A1, XREAL_1:7;
hence max (x,y) <= x + y by A4; :: thesis: verum

end;

end;

end;

hence max (x,y) <= x + y ; :: thesis: verum