theorem Th15: :: NECKLACE:16

for n being Nat st n > 0 holds
card the InternalRel of (n -SuccRelStr) = n - 1