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

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

suppose max x,y = x ; :: thesis: x = 0

hence x = 0 by A1; :: thesis: verum

end;

suppose A2: max x,y = y ; :: thesis: x = 0

then x <= y by XXREAL_0:25;
hence x = 0 by A1, A2, XXREAL_0:1; :: thesis: verum

end;

end;