theorem Th2: :: FINSEQ_2:3

for i, j being natural Number st i <= j holds
max (0,(i - j)) = 0