theorem :: NECKLACE:11

for i, j, n being Nat st i < j & j in Segm n holds
i in Segm n