theorem Th25: :: NAT_D:25

for n being natural Number holds n mod n = 0