theorem Th3: :: NECKLACE:4

for x being non zero Nat holds 0 in x