let C be Simple_closed_curve; 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; 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; ( 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) ) }
XBOOLE_0:def 10 ( { (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 ;
TARSKI:def 3 ( 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
;
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
;
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;
verum end; suppose
e in S2
;
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;
verum 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
S-Gap S = min Fproof
let e be
object ;
TARSKI:def 3 ( 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) ) }
;
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
;
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;
verum end; suppose A22:
j = len S
;
e in Fthen
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;
verum end;
end;
thus
S-Gap S = min F
by A3, XXREAL_2:9; verum