for C being Simple_closed_curve
for S being Segmentation of C
for j being Nat st 1 < j & j < (len S) -' 1 holds
Segm (S,(len S)) misses Segm (S,j)