set z = max (x,y);
x <= max (x,y) by XXREAL_0:25;
then x + (- x) <= (max (x,y)) + (- x) by XREAL_1:6;
then 0 <= (max (x,y)) - x ;
hence for b₁ being ext-real number st b₁ = (max (x,y)) - x holds
not b₁ is negative ; :: thesis: verum