theorem Th35: :: JORDAN_A:35

for C being Simple_closed_curve
for S being Segmentation of C ex F being non empty finite Subset of REAL st
( F = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Nat : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } & S-Gap S = min F )