let x, y be real number ; :: thesis: ( 0 <= x & 0 <= y implies max x,y <= x + y )
assume A1: ( 0 <= x & 0 <= y ) ; :: thesis: max x,y <= x + y

now

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

suppose A2: max x,y = x ; :: thesis: max x,y <= x + y

x + 0 <= x + y by A1, XREAL_1:9;
hence max x,y <= x + y by A2; :: thesis: verum

end;

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

y + 0 <= y + x by A1, XREAL_1:9;
hence max x,y <= x + y by A3; :: thesis: verum

end;

end;

end;

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