let i, j be Nat; :: thesis: ( i <= j implies max 0 ,(i - j) = 0 )
assume i <= j ; :: thesis: max 0 ,(i - j) = 0
then i - i <= j - i by XREAL_1:11;
then - (j - i) <= - 0 ;
hence max 0 ,(i - j) = 0 by XXREAL_0:def 10; :: thesis: verum