let x, y be Real; :: thesis: ( x >= 0 & max (x,y) = 0 implies x = 0 )
assume that
A1: x >= 0 and
A2: 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 A2; :: thesis: verum

end;

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

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

end;

end;