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 Element of NAT : ( 1 <= i & i < j & j <= len S & Segm S,i misses Segm S,j ) } and
A2: S-Gap S = min F by Th36;
S-Gap S in F by A2, XXREAL_2:def 7;
then ex i, j being Element of 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 Th8; :: thesis: verum