for i, i1 being natural Number st ( i -' i1 >= 1 or i - i1 >= 1 ) holds
(i -' i1) + i1 = i