theorem Th27: :: JORDAN_A:27

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) meets Segm (S,j)