( ( r -' s = r - s & r - s >= 0 ) or r -' s = 0 ) by Def2;
hence for b₁ being Real st b₁ = r -' s holds
not b₁ is negative by XXREAL_0:def 7; :: thesis: verum