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 )

( 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

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
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) ) }

end;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;

end;

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;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

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;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

proof

thus
S-Gap S = min F
by A3, XXREAL_2:9; :: thesis: verum
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;

end;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;

end;

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;then e in S1 by A1, A14, A15, A16, A21, A20;

hence e in F by XBOOLE_0:def 3; :: thesis: verum

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;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