let C be Simple_closed_curve; :: thesis: 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 )

let S be Segmentation of C; :: thesis: 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 )

consider S1, S2 being non empty finite Subset of REAL such that
A1: 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 ) } and
A2: S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } and
A3: S-Gap S = min ((min S1),(min S2)) by Def7;
take F = S1 \/ S2; :: thesis: ( 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 )
set X = { (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) ) } ;
thus F c= { (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) ) } :: according to XBOOLE_0:def 10 :: thesis: ( { (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) ) } c= F & S-Gap S = min F )
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in F or e in { (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) ) } )
assume A4: e in F ; :: thesis: e in { (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) ) }
per cases ( e in S1 or e in S2 ) by ;
suppose e in S1 ; :: thesis: e in { (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) ) }
then consider i, j being Element of NAT such that
A5: e = dist_min ((Segm (S,i)),(Segm (S,j))) and
A6: 1 <= i and
A7: i < j and
A8: j < len S and
Segm (S,i) misses Segm (S,j) by A6, A7, A8, A9, Th24;
hence e in { (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) ) } by A5, A6, A7, A8; :: thesis: verum
end;
suppose e in S2 ; :: thesis: e in { (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) ) }
then consider j being Element of NAT such that
A10: e = dist_min ((Segm (S,(len S))),(Segm (S,j))) and
A11: 1 < j and
A12: j < (len S) -' 1 by A2;
A13: j < len S by ;
Segm (S,(len S)) misses Segm (S,j) by ;
hence e in { (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) ) } by ; :: thesis: verum
end;
end;
end;
thus { (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) ) } c= F :: thesis:
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { (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) ) } or e in F )
assume e in { (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) ) } ; :: thesis: e in F
then consider i, j being Nat such that
A14: e = dist_min ((Segm (S,i)),(Segm (S,j))) and
A15: 1 <= i and
A16: i < j and
A17: j <= len S and
A18: Segm (S,i) misses Segm (S,j) ;
A19: i < len S by ;
A20: ( i in NAT & j in NAT ) by ORDINAL1:def 12;
per cases ( j < len S or j = len S ) by ;
end;
end;
thus S-Gap S = min F by ; :: thesis: verum