theorem Th24: :: JORDAN_A:24

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 aren't_adjacent holds
Segm (S,i) misses Segm (S,j)