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