let x, y be real number ; :: 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;