theorem :: NAT_D:40

for n being natural Number holds n -' 0 = n