for C being Simple_closed_curve
for S being Segmentation of C
for i, j being Nat st 1 <= i & i < j & j < len S & i,j are_adjacent holds
(Segm (S,i)) /\ (Segm (S,j)) = {(S /. (i + 1))}