theorem Th36: :: NAT_D:36

for n, i being natural Number st n -' i = 0 holds
n <= i