let C be Simple_closed_curve; :: thesis: for S being Segmentation of C holds S-Gap S > 0
let S be Segmentation of C; :: thesis: S-Gap S > 0
consider F being non empty finite Subset of REAL such that
A1: 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) ) } and
A2: S-Gap S = min F by Th35;
S-Gap S in F by A2, XXREAL_2:def 7;
then ex i, j being Nat st
( S-Gap S = dist_min ((Segm (S,i)),(Segm (S,j))) & 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) by A1;
hence S-Gap S > 0 by Th7; :: thesis: verum