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 Element of 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 Element of 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 & not i,j are_adjacent1 ) } 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 Element of 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 Element of 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 Element of 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 Element of 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 set ; :: 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 Element of 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 Element of 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 Element of 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 & i < j & j < len S ) and
A7: not i,j are_adjacent1 by A1;
Segm S,i misses Segm S,j by A6, A7, Th25;
hence e in { (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 ) } by A5, A6; :: thesis: verum

end;

suppose e in S2 ; :: thesis: e in { (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 ) }

then consider j being Element of NAT such that
A8: e = dist_min (Segm S,(len S)),(Segm S,j) and
A9: 1 < j and
A10: j < (len S) -' 1 by A2;
A11: j < len S by A10, NAT_D:44;
Segm S,(len S) misses Segm S,j by A9, A10, Th26;
hence e in { (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 ) } by A8, A9, A11; :: thesis: verum

end;

end;

end;

thus { (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 ) } c= F :: thesis: S-Gap S = min F

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { (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 ) } or e in F )
assume e in { (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 ) } ; :: thesis: e in F
then consider i, j being Element of NAT such that
A12: e = dist_min (Segm S,i),(Segm S,j) and
A13: 1 <= i and
A14: i < j and
A15: j <= len S and
A16: Segm S,i misses Segm S,j ;
A17: i < len S by A14, A15, XXREAL_0:2;

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

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

not i,j are_adjacent1 by A13, A14, A16, A18, Th28;
then e in S1 by A1, A12, A13, A14, A18;
hence e in F by XBOOLE_0:def 3; :: thesis: verum

end;

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

then 1 <> i by A16, Th30;
then A20: 1 < i by A13, XXREAL_0:1;
A21: i <= (len S) -' 1 by A17, NAT_D:49;
i <> (len S) -' 1 by A16, A19, Th32;
then i < (len S) -' 1 by A21, XXREAL_0:1;
then e in S2 by A2, A12, A19, 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:68; :: thesis: verum