let C be Simple_closed_curve; for S being Segmentation of C holds S-Gap S > 0
let S be Segmentation of C; 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; verum