:: deftheorem Def7 defines S-Gap JORDAN_A:def 7 :
for C being Simple_closed_curve
for S being Segmentation of C
for b₃ being Real holds
( b₃ = S-Gap S iff ex S1, S2 being non empty finite Subset of REAL st
( S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & i,j aren't_adjacent ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & b₃ = min ((min S1),(min S2)) ) );