for i, j being natural Number holds max (0,(i - j)) is Element of NAT