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 A4, XBOOLE_0:def 3;

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
A9: i,j aren't_adjacent by A1;
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 A12, NAT_D:44;
Segm (S,(len S)) misses Segm (S,j) by A11, A12, Th25;
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 A10, A11, A13; :: 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: S-Gap S = min F

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 A16, A17, XXREAL_0:2;
A20: ( i in NAT & j in NAT ) by ORDINAL1:def 12;

per cases ( j < len S or j = len S ) by A17, XXREAL_0:1;

suppose A21: j < len S ; :: thesis: e in F

i,j aren't_adjacent by A15, A16, A18, A21, Th27;
then e in S1 by A1, A14, A15, A16, A21, A20;
hence e in F by XBOOLE_0:def 3; :: thesis: verum

end;

suppose A22: j = len S ; :: thesis: e in F

then 1 <> i by A18, Th29;
then A23: 1 < i by A15, XXREAL_0:1;
A24: i <= (len S) -' 1 by A19, NAT_D:49;
i <> (len S) -' 1 by A18, A22, Th31;
then i < (len S) -' 1 by A24, XXREAL_0:1;
then e in S2 by A2, A14, A22, A23, A20;
hence e in F by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

thus S-Gap S = min F by A3, XXREAL_2:9; :: thesis: verum