theorem Th39: :: NAT_D:39

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