let C be Simple_closed_curve; for p being Point of (TOP-REAL 2) st W-bound C < p `1 & p `1 < E-bound C & p in North_Arc C holds
not p in South_Arc C
let p be Point of (TOP-REAL 2); ( W-bound C < p `1 & p `1 < E-bound C & p in North_Arc C implies not p in South_Arc C )
reconsider p9 = p as Point of (Euclid 2) by EUCLID:25;
assume that
A1:
W-bound C < p `1
and
A2:
p `1 < E-bound C
and
A3:
p in North_Arc C
and
A4:
p in South_Arc C
; contradiction
set s = min ((p `1 ) - (W-bound C)),((E-bound C) - (p `1 ));
A5:
W-bound C = (W-bound C) + 0
;
A6:
p `1 = (p `1 ) + 0
;
A7:
(p `1 ) - (W-bound C) > 0
by A1, A5, XREAL_1:22;
(E-bound C) - (p `1 ) > 0
by A2, A6, XREAL_1:22;
then A8:
min ((p `1 ) - (W-bound C)),((E-bound C) - (p `1 )) > 0
by A7, XXREAL_0:15;
now let r be
real number ;
( 0 < r & r < min ((p `1 ) - (W-bound C)),((E-bound C) - (p `1 )) implies Ball p9,r meets Upper_Arc C )reconsider rr =
r as
Real by XREAL_0:def 1;
assume that A9:
0 < r
and A10:
r < min ((p `1 ) - (W-bound C)),
((E-bound C) - (p `1 ))
;
Ball p9,r meets Upper_Arc CA11:
r / 8
> 0
by A9, XREAL_1:141;
reconsider G =
Ball p9,
(r / 8) as
a_neighborhood of
p by A9, GOBOARD6:5, XREAL_1:141;
consider k1 being
Element of
NAT such that A12:
for
m being
Element of
NAT st
m > k1 holds
(Upper_Appr C) . m meets G
by A3, KURATO_2:def 11;
consider k2 being
Element of
NAT such that A13:
for
m being
Element of
NAT st
m > k2 holds
(Lower_Appr C) . m meets G
by A4, KURATO_2:def 11;
set k =
max k1,
k2;
A14:
max k1,
k2 >= k1
by XXREAL_0:25;
set z9 =
max ((N-bound C) - (S-bound C)),
((E-bound C) - (W-bound C));
set z =
max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),
(r / 8);
(max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (r / 8) >= 1
by A11, XREAL_1:183, XXREAL_0:25;
then
log 2,
((max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (r / 8)) >= log 2,1
by PRE_FF:12;
then
log 2,
((max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (r / 8)) >= 0
by POWER:59;
then reconsider m9 =
[\(log 2,((max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (r / 8)))/] as
Element of
NAT by INT_1:80;
A15:
2
to_power (m9 + 1) > 0
by POWER:39;
set N = 2
to_power (m9 + 1);
log 2,
((max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (r / 8)) < (m9 + 1) * 1
by INT_1:52;
then
log 2,
((max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (r / 8)) < (m9 + 1) * (log 2,2)
by POWER:60;
then
log 2,
((max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (r / 8)) < log 2,
(2 to_power (m9 + 1))
by POWER:63;
then
(max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (r / 8) < 2
to_power (m9 + 1)
by A15, PRE_FF:12;
then
((max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (r / 8)) * (r / 8) < (2 to_power (m9 + 1)) * (r / 8)
by A11, XREAL_1:70;
then
max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),
(r / 8) < (2 to_power (m9 + 1)) * (r / 8)
by A11, XCMPLX_1:88;
then
(max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (2 to_power (m9 + 1)) < ((2 to_power (m9 + 1)) * (r / 8)) / (2 to_power (m9 + 1))
by A15, XREAL_1:76;
then
(max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (2 to_power (m9 + 1)) < ((r / 8) / (2 to_power (m9 + 1))) * (2 to_power (m9 + 1))
;
then A16:
(max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (2 to_power (m9 + 1)) < r / 8
by A15, XCMPLX_1:88;
(max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (2 to_power (m9 + 1)) >= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m9 + 1))
by A15, XREAL_1:74, XXREAL_0:25;
then A17:
(max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m9 + 1)) < r / 8
by A16, XXREAL_0:2;
set m =
(max (max k1,k2),m9) + 1;
A18:
len (Gauge C,((max (max k1,k2),m9) + 1)) = width (Gauge C,((max (max k1,k2),m9) + 1))
by JORDAN8:def 1;
max (max k1,k2),
m9 >= max k1,
k2
by XXREAL_0:25;
then
max (max k1,k2),
m9 >= k1
by A14, XXREAL_0:2;
then
(max (max k1,k2),m9) + 1
> k1
by NAT_1:13;
then
(Upper_Appr C) . ((max (max k1,k2),m9) + 1) meets G
by A12;
then
Upper_Arc (L~ (Cage C,((max (max k1,k2),m9) + 1))) meets G
by Def1;
then consider p1 being
set such that A19:
p1 in Upper_Arc (L~ (Cage C,((max (max k1,k2),m9) + 1)))
and A20:
p1 in G
by XBOOLE_0:3;
reconsider p1 =
p1 as
Point of
(TOP-REAL 2) by A19;
reconsider p19 =
p1 as
Point of
(Euclid 2) by EUCLID:25;
set f =
Upper_Seq C,
((max (max k1,k2),m9) + 1);
A21:
Upper_Arc (L~ (Cage C,((max (max k1,k2),m9) + 1))) = L~ (Upper_Seq C,((max (max k1,k2),m9) + 1))
by JORDAN1G:63;
then consider i1 being
Element of
NAT such that A22:
1
<= i1
and A23:
i1 + 1
<= len (Upper_Seq C,((max (max k1,k2),m9) + 1))
and A24:
p1 in LSeg ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1),
((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. (i1 + 1))
by A19, SPPOL_2:14;
reconsider c1 =
(Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1 as
Point of
(Euclid 2) by EUCLID:25;
reconsider c2 =
(Upper_Seq C,((max (max k1,k2),m9) + 1)) /. (i1 + 1) as
Point of
(Euclid 2) by EUCLID:25;
A25:
Upper_Seq C,
((max (max k1,k2),m9) + 1) is_sequence_on Gauge C,
((max (max k1,k2),m9) + 1)
by JORDAN1G:4;
i1 < len (Upper_Seq C,((max (max k1,k2),m9) + 1))
by A23, NAT_1:13;
then
i1 in Seg (len (Upper_Seq C,((max (max k1,k2),m9) + 1)))
by A22, FINSEQ_1:3;
then A26:
i1 in dom (Upper_Seq C,((max (max k1,k2),m9) + 1))
by FINSEQ_1:def 3;
then consider ii1,
jj1 being
Element of
NAT such that A27:
[ii1,jj1] in Indices (Gauge C,((max (max k1,k2),m9) + 1))
and A28:
(Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1 = (Gauge C,((max (max k1,k2),m9) + 1)) * ii1,
jj1
by A25, GOBOARD1:def 11;
A29:
N-bound C > (S-bound C) + 0
by TOPREAL5:22;
A30:
E-bound C > (W-bound C) + 0
by TOPREAL5:23;
A31:
(N-bound C) - (S-bound C) > 0
by A29, XREAL_1:22;
A32:
(E-bound C) - (W-bound C) > 0
by A30, XREAL_1:22;
A33:
2
|^ (m9 + 1) > 0
by A15, POWER:46;
max (max k1,k2),
m9 >= m9
by XXREAL_0:25;
then
(max (max k1,k2),m9) + 1
> m9
by NAT_1:13;
then
(max (max k1,k2),m9) + 1
>= m9 + 1
by NAT_1:13;
then A34:
2
|^ ((max (max k1,k2),m9) + 1) >= 2
|^ (m9 + 1)
by PREPOWER:107;
then A35:
((N-bound C) - (S-bound C)) / (2 |^ ((max (max k1,k2),m9) + 1)) <= ((N-bound C) - (S-bound C)) / (2 |^ (m9 + 1))
by A31, A33, XREAL_1:120;
A36:
((E-bound C) - (W-bound C)) / (2 |^ ((max (max k1,k2),m9) + 1)) <= ((E-bound C) - (W-bound C)) / (2 |^ (m9 + 1))
by A32, A33, A34, XREAL_1:120;
A37:
((N-bound C) - (S-bound C)) / (2 to_power (m9 + 1)) <= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m9 + 1))
by A15, XREAL_1:74, XXREAL_0:25;
A38:
((E-bound C) - (W-bound C)) / (2 to_power (m9 + 1)) <= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m9 + 1))
by A15, XREAL_1:74, XXREAL_0:25;
A39:
((N-bound C) - (S-bound C)) / (2 |^ (m9 + 1)) <= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m9 + 1))
by A37, POWER:46;
A40:
((E-bound C) - (W-bound C)) / (2 |^ (m9 + 1)) <= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m9 + 1))
by A38, POWER:46;
A41:
((N-bound C) - (S-bound C)) / (2 |^ ((max (max k1,k2),m9) + 1)) <= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m9 + 1))
by A35, A39, XXREAL_0:2;
A42:
((E-bound C) - (W-bound C)) / (2 |^ ((max (max k1,k2),m9) + 1)) <= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m9 + 1))
by A36, A40, XXREAL_0:2;
then
dist ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1),
((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. (i1 + 1)) <= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m9 + 1))
by A22, A23, A25, A41, Th6;
then
dist ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1),
((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. (i1 + 1)) < r / 8
by A17, XXREAL_0:2;
then
dist c1,
c2 < r / 8
by TOPREAL6:def 1;
then A43:
|.(((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) - ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. (i1 + 1))).| < r / 8
by SPPOL_1:62;
|.(p1 - ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1)).| <= |.(((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) - ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. (i1 + 1))).|
by A24, JGRAPH_1:53;
then A44:
|.(p1 - ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1)).| < r / 8
by A43, XXREAL_0:2;
dist p19,
p9 < r / 8
by A20, METRIC_1:12;
then
|.(p - p1).| < r / 8
by SPPOL_1:62;
then A45:
|.(p - p1).| + |.(p1 - ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1)).| < (r / (2 * 4)) + (r / (2 * 4))
by A44, XREAL_1:10;
|.(p - ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1)).| <= |.(p - p1).| + |.(p1 - ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1)).|
by TOPRNS_1:35;
then A46:
|.(p - ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1)).| < r / 4
by A45, XXREAL_0:2;
then A47:
dist p9,
c1 < r / 4
by SPPOL_1:62;
then A48:
(Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1 in Ball p9,
(r / 4)
by METRIC_1:12;
A49:
(Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1 in Upper_Arc (L~ (Cage C,((max (max k1,k2),m9) + 1)))
by A21, A26, SPPOL_2:48;
A50:
max k1,
k2 >= k2
by XXREAL_0:25;
max (max k1,k2),
m9 >= max k1,
k2
by XXREAL_0:25;
then
max (max k1,k2),
m9 >= k2
by A50, XXREAL_0:2;
then
(max (max k1,k2),m9) + 1
> k2
by NAT_1:13;
then
(Lower_Appr C) . ((max (max k1,k2),m9) + 1) meets G
by A13;
then
Lower_Arc (L~ (Cage C,((max (max k1,k2),m9) + 1))) meets G
by Def2;
then consider p2 being
set such that A51:
p2 in Lower_Arc (L~ (Cage C,((max (max k1,k2),m9) + 1)))
and A52:
p2 in G
by XBOOLE_0:3;
reconsider p2 =
p2 as
Point of
(TOP-REAL 2) by A51;
reconsider p29 =
p2 as
Point of
(Euclid 2) by EUCLID:25;
set g =
Lower_Seq C,
((max (max k1,k2),m9) + 1);
A53:
Lower_Arc (L~ (Cage C,((max (max k1,k2),m9) + 1))) = L~ (Lower_Seq C,((max (max k1,k2),m9) + 1))
by JORDAN1G:64;
then consider i2 being
Element of
NAT such that A54:
1
<= i2
and A55:
i2 + 1
<= len (Lower_Seq C,((max (max k1,k2),m9) + 1))
and A56:
p2 in LSeg ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2),
((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. (i2 + 1))
by A51, SPPOL_2:14;
reconsider d1 =
(Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2 as
Point of
(Euclid 2) by EUCLID:25;
reconsider d2 =
(Lower_Seq C,((max (max k1,k2),m9) + 1)) /. (i2 + 1) as
Point of
(Euclid 2) by EUCLID:25;
A57:
Lower_Seq C,
((max (max k1,k2),m9) + 1) is_sequence_on Gauge C,
((max (max k1,k2),m9) + 1)
by JORDAN1G:5;
i2 < len (Lower_Seq C,((max (max k1,k2),m9) + 1))
by A55, NAT_1:13;
then
i2 in Seg (len (Lower_Seq C,((max (max k1,k2),m9) + 1)))
by A54, FINSEQ_1:3;
then A58:
i2 in dom (Lower_Seq C,((max (max k1,k2),m9) + 1))
by FINSEQ_1:def 3;
then consider ii2,
jj2 being
Element of
NAT such that A59:
[ii2,jj2] in Indices (Gauge C,((max (max k1,k2),m9) + 1))
and A60:
(Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2 = (Gauge C,((max (max k1,k2),m9) + 1)) * ii2,
jj2
by A57, GOBOARD1:def 11;
dist ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2),
((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. (i2 + 1)) <= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m9 + 1))
by A41, A42, A54, A55, A57, Th6;
then
dist ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2),
((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. (i2 + 1)) < r / 8
by A17, XXREAL_0:2;
then
dist d1,
d2 < r / 8
by TOPREAL6:def 1;
then A61:
|.(((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) - ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. (i2 + 1))).| < r / 8
by SPPOL_1:62;
|.(p2 - ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2)).| <= |.(((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) - ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. (i2 + 1))).|
by A56, JGRAPH_1:53;
then A62:
|.(p2 - ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2)).| < r / 8
by A61, XXREAL_0:2;
dist p29,
p9 < r / 8
by A52, METRIC_1:12;
then
|.(p - p2).| < r / 8
by SPPOL_1:62;
then A63:
|.(p - p2).| + |.(p2 - ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2)).| < (r / (2 * 4)) + (r / (2 * 4))
by A62, XREAL_1:10;
|.(p - ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2)).| <= |.(p - p2).| + |.(p2 - ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2)).|
by TOPRNS_1:35;
then A64:
|.(p - ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2)).| < r / 4
by A63, XXREAL_0:2;
then A65:
dist p9,
d1 < r / 4
by SPPOL_1:62;
then A66:
(Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2 in Ball p9,
(r / 4)
by METRIC_1:12;
A67:
(Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2 in Lower_Arc (L~ (Cage C,((max (max k1,k2),m9) + 1)))
by A53, A58, SPPOL_2:48;
set Gij =
(Gauge C,((max (max k1,k2),m9) + 1)) * ii2,
jj1;
set Gji =
(Gauge C,((max (max k1,k2),m9) + 1)) * ii1,
jj2;
reconsider Gij9 =
(Gauge C,((max (max k1,k2),m9) + 1)) * ii2,
jj1,
Gji9 =
(Gauge C,((max (max k1,k2),m9) + 1)) * ii1,
jj2 as
Point of
(Euclid 2) by EUCLID:25;
A68:
1
<= ii1
by A27, MATRIX_1:39;
A69:
ii1 <= len (Gauge C,((max (max k1,k2),m9) + 1))
by A27, MATRIX_1:39;
A70:
1
<= jj1
by A27, MATRIX_1:39;
A71:
jj1 <= width (Gauge C,((max (max k1,k2),m9) + 1))
by A27, MATRIX_1:39;
A72:
1
<= ii2
by A59, MATRIX_1:39;
A73:
ii2 <= len (Gauge C,((max (max k1,k2),m9) + 1))
by A59, MATRIX_1:39;
A74:
1
<= jj2
by A59, MATRIX_1:39;
A75:
jj2 <= width (Gauge C,((max (max k1,k2),m9) + 1))
by A59, MATRIX_1:39;
A76:
len (Upper_Seq C,((max (max k1,k2),m9) + 1)) >= 3
by JORDAN1E:19;
A77:
len (Lower_Seq C,((max (max k1,k2),m9) + 1)) >= 3
by JORDAN1E:19;
A78:
len (Upper_Seq C,((max (max k1,k2),m9) + 1)) >= 1
by A76, XXREAL_0:2;
A79:
len (Lower_Seq C,((max (max k1,k2),m9) + 1)) >= 1
by A77, XXREAL_0:2;
A80:
len (Upper_Seq C,((max (max k1,k2),m9) + 1)) in Seg (len (Upper_Seq C,((max (max k1,k2),m9) + 1)))
by A78, FINSEQ_1:3;
A81:
len (Lower_Seq C,((max (max k1,k2),m9) + 1)) in Seg (len (Lower_Seq C,((max (max k1,k2),m9) + 1)))
by A79, FINSEQ_1:3;
A82:
len (Upper_Seq C,((max (max k1,k2),m9) + 1)) in dom (Upper_Seq C,((max (max k1,k2),m9) + 1))
by A80, FINSEQ_1:def 3;
A83:
len (Lower_Seq C,((max (max k1,k2),m9) + 1)) in dom (Lower_Seq C,((max (max k1,k2),m9) + 1))
by A81, FINSEQ_1:def 3;
A84:
r / 4
< r
by A9, XREAL_1:225;
A85:
r / 2
< r
by A9, XREAL_1:218;
A86:
min ((p `1 ) - (W-bound C)),
((E-bound C) - (p `1 )) <= (p `1 ) - (W-bound C)
by XXREAL_0:17;
A87:
min ((p `1 ) - (W-bound C)),
((E-bound C) - (p `1 )) <= (E-bound C) - (p `1 )
by XXREAL_0:17;
A88:
now assume
1
>= ii1
;
contradictionthen A89:
ii1 = 1
by A68, XXREAL_0:1;
dist p9,
c1 < r
by A47, A84, XXREAL_0:2;
then
dist p9,
c1 < min ((p `1 ) - (W-bound C)),
((E-bound C) - (p `1 ))
by A10, XXREAL_0:2;
then A90:
dist p9,
c1 < (p `1 ) - (W-bound C)
by A86, XXREAL_0:2;
A91:
(p `1 ) - (((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `1 ) <= abs ((p `1 ) - (((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `1 ))
by ABSVALUE:11;
abs ((p `1 ) - (((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `1 )) <= |.(p - ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1)).|
by JGRAPH_1:51;
then
(p `1 ) - (((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `1 ) <= |.(p - ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1)).|
by A91, XXREAL_0:2;
then
(p `1 ) - (W-bound (L~ (Cage C,((max (max k1,k2),m9) + 1)))) <= |.(p - ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1)).|
by A18, A28, A70, A71, A89, JORDAN1A:94;
then
(p `1 ) - (W-bound (L~ (Cage C,((max (max k1,k2),m9) + 1)))) <= dist p9,
c1
by SPPOL_1:62;
then
(p `1 ) - (W-bound (L~ (Cage C,((max (max k1,k2),m9) + 1)))) < (p `1 ) - (W-bound C)
by A90, XXREAL_0:2;
then
W-bound (L~ (Cage C,((max (max k1,k2),m9) + 1))) > W-bound C
by XREAL_1:15;
hence
contradiction
by Th12;
verum end; A92:
now assume
ii1 >= len (Gauge C,((max (max k1,k2),m9) + 1))
;
contradictionthen A93:
ii1 = len (Gauge C,((max (max k1,k2),m9) + 1))
by A69, XXREAL_0:1;
((Gauge C,((max (max k1,k2),m9) + 1)) * (len (Gauge C,((max (max k1,k2),m9) + 1))),jj1) `1 = E-bound (L~ (Cage C,((max (max k1,k2),m9) + 1)))
by A18, A70, A71, JORDAN1A:92;
then (Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1 =
E-max (L~ (Cage C,((max (max k1,k2),m9) + 1)))
by A21, A26, A28, A93, JORDAN1J:46, SPPOL_2:48
.=
(Upper_Seq C,((max (max k1,k2),m9) + 1)) /. (len (Upper_Seq C,((max (max k1,k2),m9) + 1)))
by JORDAN1F:7
;
then
i1 = len (Upper_Seq C,((max (max k1,k2),m9) + 1))
by A26, A82, PARTFUN2:17;
hence
contradiction
by A23, NAT_1:13;
verum end; A94:
now assume
ii2 <= 1
;
contradictionthen A95:
ii2 = 1
by A72, XXREAL_0:1;
((Gauge C,((max (max k1,k2),m9) + 1)) * 1,jj2) `1 = W-bound (L~ (Cage C,((max (max k1,k2),m9) + 1)))
by A18, A74, A75, JORDAN1A:94;
then (Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2 =
W-min (L~ (Cage C,((max (max k1,k2),m9) + 1)))
by A53, A58, A60, A95, JORDAN1J:47, SPPOL_2:48
.=
(Lower_Seq C,((max (max k1,k2),m9) + 1)) /. (len (Lower_Seq C,((max (max k1,k2),m9) + 1)))
by JORDAN1F:8
;
then
i2 = len (Lower_Seq C,((max (max k1,k2),m9) + 1))
by A58, A83, PARTFUN2:17;
hence
contradiction
by A55, NAT_1:13;
verum end; A96:
now assume
ii2 >= len (Gauge C,((max (max k1,k2),m9) + 1))
;
contradictionthen A97:
ii2 = len (Gauge C,((max (max k1,k2),m9) + 1))
by A73, XXREAL_0:1;
dist p9,
d1 < r
by A65, A84, XXREAL_0:2;
then
dist p9,
d1 < min ((p `1 ) - (W-bound C)),
((E-bound C) - (p `1 ))
by A10, XXREAL_0:2;
then A98:
dist p9,
d1 < (E-bound C) - (p `1 )
by A87, XXREAL_0:2;
A99:
(((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `1 ) - (p `1 ) <= abs ((((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `1 ) - (p `1 ))
by ABSVALUE:11;
abs ((((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `1 ) - (p `1 )) <= |.(((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) - p).|
by JGRAPH_1:51;
then
abs ((((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `1 ) - (p `1 )) <= |.(p - ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2)).|
by TOPRNS_1:28;
then
(((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `1 ) - (p `1 ) <= |.(p - ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2)).|
by A99, XXREAL_0:2;
then
(E-bound (L~ (Cage C,((max (max k1,k2),m9) + 1)))) - (p `1 ) <= |.(p - ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2)).|
by A18, A60, A74, A75, A97, JORDAN1A:92;
then
(E-bound (L~ (Cage C,((max (max k1,k2),m9) + 1)))) - (p `1 ) <= dist p9,
d1
by SPPOL_1:62;
then
(E-bound (L~ (Cage C,((max (max k1,k2),m9) + 1)))) - (p `1 ) < (E-bound C) - (p `1 )
by A98, XXREAL_0:2;
then
E-bound (L~ (Cage C,((max (max k1,k2),m9) + 1))) < E-bound C
by XREAL_1:15;
hence
contradiction
by Th10;
verum end; A100:
Ball p9,
(rr / 4) c= Ball p9,
rr
by A84, PCOMPS_1:1;
A101:
((Gauge C,((max (max k1,k2),m9) + 1)) * ii2,jj1) `1 =
((Gauge C,((max (max k1,k2),m9) + 1)) * ii2,1) `1
by A70, A71, A72, A73, GOBOARD5:3
.=
((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `1
by A60, A72, A73, A74, A75, GOBOARD5:3
;
A102:
((Gauge C,((max (max k1,k2),m9) + 1)) * ii2,jj1) `2 =
((Gauge C,((max (max k1,k2),m9) + 1)) * 1,jj1) `2
by A70, A71, A72, A73, GOBOARD5:2
.=
((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `2
by A28, A68, A69, A70, A71, GOBOARD5:2
;
A103:
((Gauge C,((max (max k1,k2),m9) + 1)) * ii1,jj2) `1 =
((Gauge C,((max (max k1,k2),m9) + 1)) * ii1,1) `1
by A68, A69, A74, A75, GOBOARD5:3
.=
((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `1
by A28, A68, A69, A70, A71, GOBOARD5:3
;
A104:
((Gauge C,((max (max k1,k2),m9) + 1)) * ii1,jj2) `2 =
((Gauge C,((max (max k1,k2),m9) + 1)) * 1,jj2) `2
by A68, A69, A74, A75, GOBOARD5:2
.=
((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `2
by A60, A72, A73, A74, A75, GOBOARD5:2
;
A105:
abs ((((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `1 ) - (p `1 )) <= |.(((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) - p).|
by JGRAPH_1:51;
A106:
abs ((((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `2 ) - (p `2 )) <= |.(((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) - p).|
by JGRAPH_1:51;
A107:
abs ((((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `1 ) - (p `1 )) <= |.(p - ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2)).|
by A105, TOPRNS_1:28;
A108:
abs ((((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `2 ) - (p `2 )) <= |.(p - ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1)).|
by A106, TOPRNS_1:28;
A109:
abs ((((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `1 ) - (p `1 )) <= r / 4
by A64, A107, XXREAL_0:2;
abs ((((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `2 ) - (p `2 )) <= r / 4
by A46, A108, XXREAL_0:2;
then
(abs ((((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `1 ) - (p `1 ))) + (abs ((((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `2 ) - (p `2 ))) <= (r / (2 * 2)) + (r / (2 * 2))
by A109, XREAL_1:9;
then A110:
(abs ((((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `1 ) - (p `1 ))) + (abs ((((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `2 ) - (p `2 ))) < r
by A85, XXREAL_0:2;
A111:
abs ((((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `1 ) - (p `1 )) <= |.(((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) - p).|
by JGRAPH_1:51;
A112:
abs ((((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `2 ) - (p `2 )) <= |.(((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) - p).|
by JGRAPH_1:51;
A113:
abs ((((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `1 ) - (p `1 )) <= |.(p - ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1)).|
by A111, TOPRNS_1:28;
A114:
abs ((((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `2 ) - (p `2 )) <= |.(p - ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2)).|
by A112, TOPRNS_1:28;
A115:
abs ((((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `1 ) - (p `1 )) <= r / 4
by A46, A113, XXREAL_0:2;
abs ((((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `2 ) - (p `2 )) <= r / 4
by A64, A114, XXREAL_0:2;
then
(abs ((((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `1 ) - (p `1 ))) + (abs ((((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `2 ) - (p `2 ))) <= (r / (2 * 2)) + (r / (2 * 2))
by A115, XREAL_1:9;
then A116:
(abs ((((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `1 ) - (p `1 ))) + (abs ((((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `2 ) - (p `2 ))) < r
by A85, XXREAL_0:2;
|.(((Gauge C,((max (max k1,k2),m9) + 1)) * ii2,jj1) - p).| <= (abs ((((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `1 ) - (p `1 ))) + (abs ((((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `2 ) - (p `2 )))
by A101, A102, JGRAPH_1:49;
then
|.(((Gauge C,((max (max k1,k2),m9) + 1)) * ii2,jj1) - p).| < r
by A110, XXREAL_0:2;
then
dist Gij9,
p9 < r
by SPPOL_1:62;
then A117:
(Gauge C,((max (max k1,k2),m9) + 1)) * ii2,
jj1 in Ball p9,
r
by METRIC_1:12;
|.(((Gauge C,((max (max k1,k2),m9) + 1)) * ii1,jj2) - p).| <= (abs ((((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `1 ) - (p `1 ))) + (abs ((((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `2 ) - (p `2 )))
by A103, A104, JGRAPH_1:49;
then
|.(((Gauge C,((max (max k1,k2),m9) + 1)) * ii1,jj2) - p).| < r
by A116, XXREAL_0:2;
then
dist Gji9,
p9 < r
by SPPOL_1:62;
then A118:
(Gauge C,((max (max k1,k2),m9) + 1)) * ii1,
jj2 in Ball p9,
r
by METRIC_1:12;
A119:
LSeg ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2),
((Gauge C,((max (max k1,k2),m9) + 1)) * ii2,jj1) c= Ball p9,
rr
by A66, A100, A117, TOPREAL3:28;
A120:
LSeg ((Gauge C,((max (max k1,k2),m9) + 1)) * ii2,jj1),
((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) c= Ball p9,
rr
by A48, A100, A117, TOPREAL3:28;
A121:
LSeg ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2),
((Gauge C,((max (max k1,k2),m9) + 1)) * ii1,jj2) c= Ball p9,
rr
by A66, A100, A118, TOPREAL3:28;
A122:
LSeg ((Gauge C,((max (max k1,k2),m9) + 1)) * ii1,jj2),
((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) c= Ball p9,
rr
by A48, A100, A118, TOPREAL3:28;
now per cases
( jj2 <= jj1 or jj1 < jj2 )
;
suppose A123:
jj2 <= jj1
;
Ball p9,r meets Upper_Arc C
(LSeg ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2),((Gauge C,((max (max k1,k2),m9) + 1)) * ii2,jj1)) \/ (LSeg ((Gauge C,((max (max k1,k2),m9) + 1)) * ii2,jj1),((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1)) c= Ball p9,
r
proof
let x be
set ;
TARSKI:def 3 ( not x in (LSeg ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2),((Gauge C,((max (max k1,k2),m9) + 1)) * ii2,jj1)) \/ (LSeg ((Gauge C,((max (max k1,k2),m9) + 1)) * ii2,jj1),((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1)) or x in Ball p9,r )
assume A124:
x in (LSeg ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2),((Gauge C,((max (max k1,k2),m9) + 1)) * ii2,jj1)) \/ (LSeg ((Gauge C,((max (max k1,k2),m9) + 1)) * ii2,jj1),((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1))
;
x in Ball p9,r
then reconsider x9 =
x as
Point of
(TOP-REAL 2) ;
now per cases
( x9 in LSeg ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2),((Gauge C,((max (max k1,k2),m9) + 1)) * ii2,jj1) or x9 in LSeg ((Gauge C,((max (max k1,k2),m9) + 1)) * ii2,jj1),((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) )
by A124, XBOOLE_0:def 3;
end;
hence
x in Ball p9,
r
;
verum
end; hence
Ball p9,
r meets Upper_Arc C
by A28, A49, A60, A67, A71, A74, A88, A92, A94, A96, A123, JORDAN15:50, XBOOLE_1:63;
verum end; suppose A125:
jj1 < jj2
;
Ball p9,r meets Upper_Arc C
(LSeg ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1),((Gauge C,((max (max k1,k2),m9) + 1)) * ii1,jj2)) \/ (LSeg ((Gauge C,((max (max k1,k2),m9) + 1)) * ii1,jj2),((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2)) c= Ball p9,
r
proof
let x be
set ;
TARSKI:def 3 ( not x in (LSeg ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1),((Gauge C,((max (max k1,k2),m9) + 1)) * ii1,jj2)) \/ (LSeg ((Gauge C,((max (max k1,k2),m9) + 1)) * ii1,jj2),((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2)) or x in Ball p9,r )
assume A126:
x in (LSeg ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1),((Gauge C,((max (max k1,k2),m9) + 1)) * ii1,jj2)) \/ (LSeg ((Gauge C,((max (max k1,k2),m9) + 1)) * ii1,jj2),((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2))
;
x in Ball p9,r
then reconsider x9 =
x as
Point of
(TOP-REAL 2) ;
now per cases
( x9 in LSeg ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1),((Gauge C,((max (max k1,k2),m9) + 1)) * ii1,jj2) or x9 in LSeg ((Gauge C,((max (max k1,k2),m9) + 1)) * ii1,jj2),((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) )
by A126, XBOOLE_0:def 3;
end;
hence
x in Ball p9,
r
;
verum
end; hence
Ball p9,
r meets Upper_Arc C
by A28, A49, A60, A67, A70, A75, A88, A92, A94, A96, A125, Th26, XBOOLE_1:63;
verum end; hence
Ball p9,
r meets Upper_Arc C
;
verum end;
then
p in Cl (Upper_Arc C)
by A8, GOBOARD6:96;
then A127:
p in Upper_Arc C
by PRE_TOPC:52;
now let r be
real number ;
( 0 < r & r < min ((p `1 ) - (W-bound C)),((E-bound C) - (p `1 )) implies Ball p9,r meets Lower_Arc C )reconsider rr =
r as
Real by XREAL_0:def 1;
assume that A128:
0 < r
and A129:
r < min ((p `1 ) - (W-bound C)),
((E-bound C) - (p `1 ))
;
Ball p9,r meets Lower_Arc CA130:
r / 8
> 0
by A128, XREAL_1:141;
reconsider G =
Ball p9,
(r / 8) as
a_neighborhood of
p by A128, GOBOARD6:5, XREAL_1:141;
consider k1 being
Element of
NAT such that A131:
for
m being
Element of
NAT st
m > k1 holds
(Upper_Appr C) . m meets G
by A3, KURATO_2:def 11;
consider k2 being
Element of
NAT such that A132:
for
m being
Element of
NAT st
m > k2 holds
(Lower_Appr C) . m meets G
by A4, KURATO_2:def 11;
set k =
max k1,
k2;
A133:
max k1,
k2 >= k1
by XXREAL_0:25;
set z9 =
max ((N-bound C) - (S-bound C)),
((E-bound C) - (W-bound C));
set z =
max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),
(r / 8);
(max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (r / 8) >= 1
by A130, XREAL_1:183, XXREAL_0:25;
then
log 2,
((max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (r / 8)) >= log 2,1
by PRE_FF:12;
then
log 2,
((max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (r / 8)) >= 0
by POWER:59;
then reconsider m9 =
[\(log 2,((max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (r / 8)))/] as
Element of
NAT by INT_1:80;
A134:
2
to_power (m9 + 1) > 0
by POWER:39;
set N = 2
to_power (m9 + 1);
log 2,
((max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (r / 8)) < (m9 + 1) * 1
by INT_1:52;
then
log 2,
((max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (r / 8)) < (m9 + 1) * (log 2,2)
by POWER:60;
then
log 2,
((max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (r / 8)) < log 2,
(2 to_power (m9 + 1))
by POWER:63;
then
(max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (r / 8) < 2
to_power (m9 + 1)
by A134, PRE_FF:12;
then
((max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (r / 8)) * (r / 8) < (2 to_power (m9 + 1)) * (r / 8)
by A130, XREAL_1:70;
then
max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),
(r / 8) < (2 to_power (m9 + 1)) * (r / 8)
by A130, XCMPLX_1:88;
then
(max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (2 to_power (m9 + 1)) < ((2 to_power (m9 + 1)) * (r / 8)) / (2 to_power (m9 + 1))
by A134, XREAL_1:76;
then
(max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (2 to_power (m9 + 1)) < ((r / 8) / (2 to_power (m9 + 1))) * (2 to_power (m9 + 1))
;
then A135:
(max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (2 to_power (m9 + 1)) < r / 8
by A134, XCMPLX_1:88;
(max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (2 to_power (m9 + 1)) >= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m9 + 1))
by A134, XREAL_1:74, XXREAL_0:25;
then A136:
(max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m9 + 1)) < r / 8
by A135, XXREAL_0:2;
set m =
(max (max k1,k2),m9) + 1;
A137:
len (Gauge C,((max (max k1,k2),m9) + 1)) = width (Gauge C,((max (max k1,k2),m9) + 1))
by JORDAN8:def 1;
max (max k1,k2),
m9 >= max k1,
k2
by XXREAL_0:25;
then
max (max k1,k2),
m9 >= k1
by A133, XXREAL_0:2;
then
(max (max k1,k2),m9) + 1
> k1
by NAT_1:13;
then
(Upper_Appr C) . ((max (max k1,k2),m9) + 1) meets G
by A131;
then
Upper_Arc (L~ (Cage C,((max (max k1,k2),m9) + 1))) meets G
by Def1;
then consider p1 being
set such that A138:
p1 in Upper_Arc (L~ (Cage C,((max (max k1,k2),m9) + 1)))
and A139:
p1 in G
by XBOOLE_0:3;
reconsider p1 =
p1 as
Point of
(TOP-REAL 2) by A138;
reconsider p19 =
p1 as
Point of
(Euclid 2) by EUCLID:25;
set f =
Upper_Seq C,
((max (max k1,k2),m9) + 1);
A140:
Upper_Arc (L~ (Cage C,((max (max k1,k2),m9) + 1))) = L~ (Upper_Seq C,((max (max k1,k2),m9) + 1))
by JORDAN1G:63;
then consider i1 being
Element of
NAT such that A141:
1
<= i1
and A142:
i1 + 1
<= len (Upper_Seq C,((max (max k1,k2),m9) + 1))
and A143:
p1 in LSeg ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1),
((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. (i1 + 1))
by A138, SPPOL_2:14;
reconsider c1 =
(Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1 as
Point of
(Euclid 2) by EUCLID:25;
reconsider c2 =
(Upper_Seq C,((max (max k1,k2),m9) + 1)) /. (i1 + 1) as
Point of
(Euclid 2) by EUCLID:25;
A144:
Upper_Seq C,
((max (max k1,k2),m9) + 1) is_sequence_on Gauge C,
((max (max k1,k2),m9) + 1)
by JORDAN1G:4;
i1 < len (Upper_Seq C,((max (max k1,k2),m9) + 1))
by A142, NAT_1:13;
then
i1 in Seg (len (Upper_Seq C,((max (max k1,k2),m9) + 1)))
by A141, FINSEQ_1:3;
then A145:
i1 in dom (Upper_Seq C,((max (max k1,k2),m9) + 1))
by FINSEQ_1:def 3;
then consider ii1,
jj1 being
Element of
NAT such that A146:
[ii1,jj1] in Indices (Gauge C,((max (max k1,k2),m9) + 1))
and A147:
(Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1 = (Gauge C,((max (max k1,k2),m9) + 1)) * ii1,
jj1
by A144, GOBOARD1:def 11;
A148:
N-bound C > (S-bound C) + 0
by TOPREAL5:22;
A149:
E-bound C > (W-bound C) + 0
by TOPREAL5:23;
A150:
(N-bound C) - (S-bound C) > 0
by A148, XREAL_1:22;
A151:
(E-bound C) - (W-bound C) > 0
by A149, XREAL_1:22;
A152:
2
|^ (m9 + 1) > 0
by A134, POWER:46;
max (max k1,k2),
m9 >= m9
by XXREAL_0:25;
then
(max (max k1,k2),m9) + 1
> m9
by NAT_1:13;
then
(max (max k1,k2),m9) + 1
>= m9 + 1
by NAT_1:13;
then A153:
2
|^ ((max (max k1,k2),m9) + 1) >= 2
|^ (m9 + 1)
by PREPOWER:107;
then A154:
((N-bound C) - (S-bound C)) / (2 |^ ((max (max k1,k2),m9) + 1)) <= ((N-bound C) - (S-bound C)) / (2 |^ (m9 + 1))
by A150, A152, XREAL_1:120;
A155:
((E-bound C) - (W-bound C)) / (2 |^ ((max (max k1,k2),m9) + 1)) <= ((E-bound C) - (W-bound C)) / (2 |^ (m9 + 1))
by A151, A152, A153, XREAL_1:120;
A156:
((N-bound C) - (S-bound C)) / (2 to_power (m9 + 1)) <= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m9 + 1))
by A134, XREAL_1:74, XXREAL_0:25;
A157:
((E-bound C) - (W-bound C)) / (2 to_power (m9 + 1)) <= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m9 + 1))
by A134, XREAL_1:74, XXREAL_0:25;
A158:
((N-bound C) - (S-bound C)) / (2 |^ (m9 + 1)) <= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m9 + 1))
by A156, POWER:46;
A159:
((E-bound C) - (W-bound C)) / (2 |^ (m9 + 1)) <= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m9 + 1))
by A157, POWER:46;
A160:
((N-bound C) - (S-bound C)) / (2 |^ ((max (max k1,k2),m9) + 1)) <= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m9 + 1))
by A154, A158, XXREAL_0:2;
A161:
((E-bound C) - (W-bound C)) / (2 |^ ((max (max k1,k2),m9) + 1)) <= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m9 + 1))
by A155, A159, XXREAL_0:2;
then
dist ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1),
((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. (i1 + 1)) <= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m9 + 1))
by A141, A142, A144, A160, Th6;
then
dist ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1),
((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. (i1 + 1)) < r / 8
by A136, XXREAL_0:2;
then
dist c1,
c2 < r / 8
by TOPREAL6:def 1;
then A162:
|.(((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) - ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. (i1 + 1))).| < r / 8
by SPPOL_1:62;
|.(p1 - ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1)).| <= |.(((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) - ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. (i1 + 1))).|
by A143, JGRAPH_1:53;
then A163:
|.(p1 - ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1)).| < r / 8
by A162, XXREAL_0:2;
dist p19,
p9 < r / 8
by A139, METRIC_1:12;
then
|.(p - p1).| < r / 8
by SPPOL_1:62;
then A164:
|.(p - p1).| + |.(p1 - ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1)).| < (r / (2 * 4)) + (r / (2 * 4))
by A163, XREAL_1:10;
|.(p - ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1)).| <= |.(p - p1).| + |.(p1 - ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1)).|
by TOPRNS_1:35;
then A165:
|.(p - ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1)).| < r / 4
by A164, XXREAL_0:2;
then A166:
dist p9,
c1 < r / 4
by SPPOL_1:62;
then A167:
(Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1 in Ball p9,
(r / 4)
by METRIC_1:12;
A168:
(Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1 in Upper_Arc (L~ (Cage C,((max (max k1,k2),m9) + 1)))
by A140, A145, SPPOL_2:48;
A169:
max k1,
k2 >= k2
by XXREAL_0:25;
max (max k1,k2),
m9 >= max k1,
k2
by XXREAL_0:25;
then
max (max k1,k2),
m9 >= k2
by A169, XXREAL_0:2;
then
(max (max k1,k2),m9) + 1
> k2
by NAT_1:13;
then
(Lower_Appr C) . ((max (max k1,k2),m9) + 1) meets G
by A132;
then
Lower_Arc (L~ (Cage C,((max (max k1,k2),m9) + 1))) meets G
by Def2;
then consider p2 being
set such that A170:
p2 in Lower_Arc (L~ (Cage C,((max (max k1,k2),m9) + 1)))
and A171:
p2 in G
by XBOOLE_0:3;
reconsider p2 =
p2 as
Point of
(TOP-REAL 2) by A170;
reconsider p29 =
p2 as
Point of
(Euclid 2) by EUCLID:25;
set g =
Lower_Seq C,
((max (max k1,k2),m9) + 1);
A172:
Lower_Arc (L~ (Cage C,((max (max k1,k2),m9) + 1))) = L~ (Lower_Seq C,((max (max k1,k2),m9) + 1))
by JORDAN1G:64;
then consider i2 being
Element of
NAT such that A173:
1
<= i2
and A174:
i2 + 1
<= len (Lower_Seq C,((max (max k1,k2),m9) + 1))
and A175:
p2 in LSeg ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2),
((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. (i2 + 1))
by A170, SPPOL_2:14;
reconsider d1 =
(Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2 as
Point of
(Euclid 2) by EUCLID:25;
reconsider d2 =
(Lower_Seq C,((max (max k1,k2),m9) + 1)) /. (i2 + 1) as
Point of
(Euclid 2) by EUCLID:25;
A176:
Lower_Seq C,
((max (max k1,k2),m9) + 1) is_sequence_on Gauge C,
((max (max k1,k2),m9) + 1)
by JORDAN1G:5;
i2 < len (Lower_Seq C,((max (max k1,k2),m9) + 1))
by A174, NAT_1:13;
then
i2 in Seg (len (Lower_Seq C,((max (max k1,k2),m9) + 1)))
by A173, FINSEQ_1:3;
then A177:
i2 in dom (Lower_Seq C,((max (max k1,k2),m9) + 1))
by FINSEQ_1:def 3;
then consider ii2,
jj2 being
Element of
NAT such that A178:
[ii2,jj2] in Indices (Gauge C,((max (max k1,k2),m9) + 1))
and A179:
(Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2 = (Gauge C,((max (max k1,k2),m9) + 1)) * ii2,
jj2
by A176, GOBOARD1:def 11;
dist ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2),
((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. (i2 + 1)) <= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m9 + 1))
by A160, A161, A173, A174, A176, Th6;
then
dist ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2),
((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. (i2 + 1)) < r / 8
by A136, XXREAL_0:2;
then
dist d1,
d2 < r / 8
by TOPREAL6:def 1;
then A180:
|.(((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) - ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. (i2 + 1))).| < r / 8
by SPPOL_1:62;
|.(p2 - ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2)).| <= |.(((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) - ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. (i2 + 1))).|
by A175, JGRAPH_1:53;
then A181:
|.(p2 - ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2)).| < r / 8
by A180, XXREAL_0:2;
dist p29,
p9 < r / 8
by A171, METRIC_1:12;
then
|.(p - p2).| < r / 8
by SPPOL_1:62;
then A182:
|.(p - p2).| + |.(p2 - ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2)).| < (r / (2 * 4)) + (r / (2 * 4))
by A181, XREAL_1:10;
|.(p - ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2)).| <= |.(p - p2).| + |.(p2 - ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2)).|
by TOPRNS_1:35;
then A183:
|.(p - ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2)).| < r / 4
by A182, XXREAL_0:2;
then A184:
dist p9,
d1 < r / 4
by SPPOL_1:62;
then A185:
(Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2 in Ball p9,
(r / 4)
by METRIC_1:12;
A186:
(Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2 in Lower_Arc (L~ (Cage C,((max (max k1,k2),m9) + 1)))
by A172, A177, SPPOL_2:48;
set Gij =
(Gauge C,((max (max k1,k2),m9) + 1)) * ii2,
jj1;
set Gji =
(Gauge C,((max (max k1,k2),m9) + 1)) * ii1,
jj2;
reconsider Gij9 =
(Gauge C,((max (max k1,k2),m9) + 1)) * ii2,
jj1,
Gji9 =
(Gauge C,((max (max k1,k2),m9) + 1)) * ii1,
jj2 as
Point of
(Euclid 2) by EUCLID:25;
A187:
1
<= ii1
by A146, MATRIX_1:39;
A188:
ii1 <= len (Gauge C,((max (max k1,k2),m9) + 1))
by A146, MATRIX_1:39;
A189:
1
<= jj1
by A146, MATRIX_1:39;
A190:
jj1 <= width (Gauge C,((max (max k1,k2),m9) + 1))
by A146, MATRIX_1:39;
A191:
1
<= ii2
by A178, MATRIX_1:39;
A192:
ii2 <= len (Gauge C,((max (max k1,k2),m9) + 1))
by A178, MATRIX_1:39;
A193:
1
<= jj2
by A178, MATRIX_1:39;
A194:
jj2 <= width (Gauge C,((max (max k1,k2),m9) + 1))
by A178, MATRIX_1:39;
A195:
len (Upper_Seq C,((max (max k1,k2),m9) + 1)) >= 3
by JORDAN1E:19;
A196:
len (Lower_Seq C,((max (max k1,k2),m9) + 1)) >= 3
by JORDAN1E:19;
A197:
len (Upper_Seq C,((max (max k1,k2),m9) + 1)) >= 1
by A195, XXREAL_0:2;
A198:
len (Lower_Seq C,((max (max k1,k2),m9) + 1)) >= 1
by A196, XXREAL_0:2;
A199:
len (Upper_Seq C,((max (max k1,k2),m9) + 1)) in Seg (len (Upper_Seq C,((max (max k1,k2),m9) + 1)))
by A197, FINSEQ_1:3;
A200:
len (Lower_Seq C,((max (max k1,k2),m9) + 1)) in Seg (len (Lower_Seq C,((max (max k1,k2),m9) + 1)))
by A198, FINSEQ_1:3;
A201:
len (Upper_Seq C,((max (max k1,k2),m9) + 1)) in dom (Upper_Seq C,((max (max k1,k2),m9) + 1))
by A199, FINSEQ_1:def 3;
A202:
len (Lower_Seq C,((max (max k1,k2),m9) + 1)) in dom (Lower_Seq C,((max (max k1,k2),m9) + 1))
by A200, FINSEQ_1:def 3;
A203:
r / 4
< r
by A128, XREAL_1:225;
A204:
r / 2
< r
by A128, XREAL_1:218;
A205:
min ((p `1 ) - (W-bound C)),
((E-bound C) - (p `1 )) <= (p `1 ) - (W-bound C)
by XXREAL_0:17;
A206:
min ((p `1 ) - (W-bound C)),
((E-bound C) - (p `1 )) <= (E-bound C) - (p `1 )
by XXREAL_0:17;
A207:
now assume
1
>= ii1
;
contradictionthen A208:
ii1 = 1
by A187, XXREAL_0:1;
dist p9,
c1 < r
by A166, A203, XXREAL_0:2;
then
dist p9,
c1 < min ((p `1 ) - (W-bound C)),
((E-bound C) - (p `1 ))
by A129, XXREAL_0:2;
then A209:
dist p9,
c1 < (p `1 ) - (W-bound C)
by A205, XXREAL_0:2;
A210:
(p `1 ) - (((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `1 ) <= abs ((p `1 ) - (((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `1 ))
by ABSVALUE:11;
abs ((p `1 ) - (((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `1 )) <= |.(p - ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1)).|
by JGRAPH_1:51;
then
(p `1 ) - (((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `1 ) <= |.(p - ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1)).|
by A210, XXREAL_0:2;
then
(p `1 ) - (W-bound (L~ (Cage C,((max (max k1,k2),m9) + 1)))) <= |.(p - ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1)).|
by A137, A147, A189, A190, A208, JORDAN1A:94;
then
(p `1 ) - (W-bound (L~ (Cage C,((max (max k1,k2),m9) + 1)))) <= dist p9,
c1
by SPPOL_1:62;
then
(p `1 ) - (W-bound (L~ (Cage C,((max (max k1,k2),m9) + 1)))) < (p `1 ) - (W-bound C)
by A209, XXREAL_0:2;
then
W-bound (L~ (Cage C,((max (max k1,k2),m9) + 1))) > W-bound C
by XREAL_1:15;
hence
contradiction
by Th12;
verum end; A211:
now assume
ii1 >= len (Gauge C,((max (max k1,k2),m9) + 1))
;
contradictionthen A212:
ii1 = len (Gauge C,((max (max k1,k2),m9) + 1))
by A188, XXREAL_0:1;
((Gauge C,((max (max k1,k2),m9) + 1)) * (len (Gauge C,((max (max k1,k2),m9) + 1))),jj1) `1 = E-bound (L~ (Cage C,((max (max k1,k2),m9) + 1)))
by A137, A189, A190, JORDAN1A:92;
then (Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1 =
E-max (L~ (Cage C,((max (max k1,k2),m9) + 1)))
by A140, A145, A147, A212, JORDAN1J:46, SPPOL_2:48
.=
(Upper_Seq C,((max (max k1,k2),m9) + 1)) /. (len (Upper_Seq C,((max (max k1,k2),m9) + 1)))
by JORDAN1F:7
;
then
i1 = len (Upper_Seq C,((max (max k1,k2),m9) + 1))
by A145, A201, PARTFUN2:17;
hence
contradiction
by A142, NAT_1:13;
verum end; A213:
now assume
ii2 <= 1
;
contradictionthen A214:
ii2 = 1
by A191, XXREAL_0:1;
((Gauge C,((max (max k1,k2),m9) + 1)) * 1,jj2) `1 = W-bound (L~ (Cage C,((max (max k1,k2),m9) + 1)))
by A137, A193, A194, JORDAN1A:94;
then (Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2 =
W-min (L~ (Cage C,((max (max k1,k2),m9) + 1)))
by A172, A177, A179, A214, JORDAN1J:47, SPPOL_2:48
.=
(Lower_Seq C,((max (max k1,k2),m9) + 1)) /. (len (Lower_Seq C,((max (max k1,k2),m9) + 1)))
by JORDAN1F:8
;
then
i2 = len (Lower_Seq C,((max (max k1,k2),m9) + 1))
by A177, A202, PARTFUN2:17;
hence
contradiction
by A174, NAT_1:13;
verum end; A215:
now assume
ii2 >= len (Gauge C,((max (max k1,k2),m9) + 1))
;
contradictionthen A216:
ii2 = len (Gauge C,((max (max k1,k2),m9) + 1))
by A192, XXREAL_0:1;
dist p9,
d1 < r
by A184, A203, XXREAL_0:2;
then
dist p9,
d1 < min ((p `1 ) - (W-bound C)),
((E-bound C) - (p `1 ))
by A129, XXREAL_0:2;
then A217:
dist p9,
d1 < (E-bound C) - (p `1 )
by A206, XXREAL_0:2;
A218:
(((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `1 ) - (p `1 ) <= abs ((((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `1 ) - (p `1 ))
by ABSVALUE:11;
abs ((((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `1 ) - (p `1 )) <= |.(((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) - p).|
by JGRAPH_1:51;
then
abs ((((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `1 ) - (p `1 )) <= |.(p - ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2)).|
by TOPRNS_1:28;
then
(((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `1 ) - (p `1 ) <= |.(p - ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2)).|
by A218, XXREAL_0:2;
then
(E-bound (L~ (Cage C,((max (max k1,k2),m9) + 1)))) - (p `1 ) <= |.(p - ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2)).|
by A137, A179, A193, A194, A216, JORDAN1A:92;
then
(E-bound (L~ (Cage C,((max (max k1,k2),m9) + 1)))) - (p `1 ) <= dist p9,
d1
by SPPOL_1:62;
then
(E-bound (L~ (Cage C,((max (max k1,k2),m9) + 1)))) - (p `1 ) < (E-bound C) - (p `1 )
by A217, XXREAL_0:2;
then
E-bound (L~ (Cage C,((max (max k1,k2),m9) + 1))) < E-bound C
by XREAL_1:15;
hence
contradiction
by Th10;
verum end; A219:
Ball p9,
(rr / 4) c= Ball p9,
rr
by A203, PCOMPS_1:1;
A220:
((Gauge C,((max (max k1,k2),m9) + 1)) * ii2,jj1) `1 =
((Gauge C,((max (max k1,k2),m9) + 1)) * ii2,1) `1
by A189, A190, A191, A192, GOBOARD5:3
.=
((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `1
by A179, A191, A192, A193, A194, GOBOARD5:3
;
A221:
((Gauge C,((max (max k1,k2),m9) + 1)) * ii2,jj1) `2 =
((Gauge C,((max (max k1,k2),m9) + 1)) * 1,jj1) `2
by A189, A190, A191, A192, GOBOARD5:2
.=
((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `2
by A147, A187, A188, A189, A190, GOBOARD5:2
;
A222:
((Gauge C,((max (max k1,k2),m9) + 1)) * ii1,jj2) `1 =
((Gauge C,((max (max k1,k2),m9) + 1)) * ii1,1) `1
by A187, A188, A193, A194, GOBOARD5:3
.=
((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `1
by A147, A187, A188, A189, A190, GOBOARD5:3
;
A223:
((Gauge C,((max (max k1,k2),m9) + 1)) * ii1,jj2) `2 =
((Gauge C,((max (max k1,k2),m9) + 1)) * 1,jj2) `2
by A187, A188, A193, A194, GOBOARD5:2
.=
((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `2
by A179, A191, A192, A193, A194, GOBOARD5:2
;
A224:
abs ((((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `1 ) - (p `1 )) <= |.(((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) - p).|
by JGRAPH_1:51;
A225:
abs ((((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `2 ) - (p `2 )) <= |.(((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) - p).|
by JGRAPH_1:51;
A226:
abs ((((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `1 ) - (p `1 )) <= |.(p - ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2)).|
by A224, TOPRNS_1:28;
A227:
abs ((((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `2 ) - (p `2 )) <= |.(p - ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1)).|
by A225, TOPRNS_1:28;
A228:
abs ((((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `1 ) - (p `1 )) <= r / 4
by A183, A226, XXREAL_0:2;
abs ((((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `2 ) - (p `2 )) <= r / 4
by A165, A227, XXREAL_0:2;
then
(abs ((((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `1 ) - (p `1 ))) + (abs ((((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `2 ) - (p `2 ))) <= (r / (2 * 2)) + (r / (2 * 2))
by A228, XREAL_1:9;
then A229:
(abs ((((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `1 ) - (p `1 ))) + (abs ((((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `2 ) - (p `2 ))) < r
by A204, XXREAL_0:2;
A230:
abs ((((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `1 ) - (p `1 )) <= |.(((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) - p).|
by JGRAPH_1:51;
A231:
abs ((((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `2 ) - (p `2 )) <= |.(((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) - p).|
by JGRAPH_1:51;
A232:
abs ((((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `1 ) - (p `1 )) <= |.(p - ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1)).|
by A230, TOPRNS_1:28;
A233:
abs ((((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `2 ) - (p `2 )) <= |.(p - ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2)).|
by A231, TOPRNS_1:28;
A234:
abs ((((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `1 ) - (p `1 )) <= r / 4
by A165, A232, XXREAL_0:2;
abs ((((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `2 ) - (p `2 )) <= r / 4
by A183, A233, XXREAL_0:2;
then
(abs ((((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `1 ) - (p `1 ))) + (abs ((((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `2 ) - (p `2 ))) <= (r / (2 * 2)) + (r / (2 * 2))
by A234, XREAL_1:9;
then A235:
(abs ((((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `1 ) - (p `1 ))) + (abs ((((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `2 ) - (p `2 ))) < r
by A204, XXREAL_0:2;
|.(((Gauge C,((max (max k1,k2),m9) + 1)) * ii2,jj1) - p).| <= (abs ((((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `1 ) - (p `1 ))) + (abs ((((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `2 ) - (p `2 )))
by A220, A221, JGRAPH_1:49;
then
|.(((Gauge C,((max (max k1,k2),m9) + 1)) * ii2,jj1) - p).| < r
by A229, XXREAL_0:2;
then
dist Gij9,
p9 < r
by SPPOL_1:62;
then A236:
(Gauge C,((max (max k1,k2),m9) + 1)) * ii2,
jj1 in Ball p9,
r
by METRIC_1:12;
|.(((Gauge C,((max (max k1,k2),m9) + 1)) * ii1,jj2) - p).| <= (abs ((((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) `1 ) - (p `1 ))) + (abs ((((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) `2 ) - (p `2 )))
by A222, A223, JGRAPH_1:49;
then
|.(((Gauge C,((max (max k1,k2),m9) + 1)) * ii1,jj2) - p).| < r
by A235, XXREAL_0:2;
then
dist Gji9,
p9 < r
by SPPOL_1:62;
then A237:
(Gauge C,((max (max k1,k2),m9) + 1)) * ii1,
jj2 in Ball p9,
r
by METRIC_1:12;
A238:
LSeg ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2),
((Gauge C,((max (max k1,k2),m9) + 1)) * ii2,jj1) c= Ball p9,
rr
by A185, A219, A236, TOPREAL3:28;
A239:
LSeg ((Gauge C,((max (max k1,k2),m9) + 1)) * ii2,jj1),
((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) c= Ball p9,
rr
by A167, A219, A236, TOPREAL3:28;
A240:
LSeg ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2),
((Gauge C,((max (max k1,k2),m9) + 1)) * ii1,jj2) c= Ball p9,
rr
by A185, A219, A237, TOPREAL3:28;
A241:
LSeg ((Gauge C,((max (max k1,k2),m9) + 1)) * ii1,jj2),
((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) c= Ball p9,
rr
by A167, A219, A237, TOPREAL3:28;
now per cases
( jj2 <= jj1 or jj1 < jj2 )
;
suppose A242:
jj2 <= jj1
;
Ball p9,r meets Lower_Arc C
(LSeg ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2),((Gauge C,((max (max k1,k2),m9) + 1)) * ii2,jj1)) \/ (LSeg ((Gauge C,((max (max k1,k2),m9) + 1)) * ii2,jj1),((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1)) c= Ball p9,
r
proof
let x be
set ;
TARSKI:def 3 ( not x in (LSeg ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2),((Gauge C,((max (max k1,k2),m9) + 1)) * ii2,jj1)) \/ (LSeg ((Gauge C,((max (max k1,k2),m9) + 1)) * ii2,jj1),((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1)) or x in Ball p9,r )
assume A243:
x in (LSeg ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2),((Gauge C,((max (max k1,k2),m9) + 1)) * ii2,jj1)) \/ (LSeg ((Gauge C,((max (max k1,k2),m9) + 1)) * ii2,jj1),((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1))
;
x in Ball p9,r
then reconsider x9 =
x as
Point of
(TOP-REAL 2) ;
now per cases
( x9 in LSeg ((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2),((Gauge C,((max (max k1,k2),m9) + 1)) * ii2,jj1) or x9 in LSeg ((Gauge C,((max (max k1,k2),m9) + 1)) * ii2,jj1),((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1) )
by A243, XBOOLE_0:def 3;
end;
hence
x in Ball p9,
r
;
verum
end; hence
Ball p9,
r meets Lower_Arc C
by A147, A168, A179, A186, A190, A193, A207, A211, A213, A215, A242, JORDAN15:51, XBOOLE_1:63;
verum end; suppose A244:
jj1 < jj2
;
Ball p9,r meets Lower_Arc C
(LSeg ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1),((Gauge C,((max (max k1,k2),m9) + 1)) * ii1,jj2)) \/ (LSeg ((Gauge C,((max (max k1,k2),m9) + 1)) * ii1,jj2),((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2)) c= Ball p9,
r
proof
let x be
set ;
TARSKI:def 3 ( not x in (LSeg ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1),((Gauge C,((max (max k1,k2),m9) + 1)) * ii1,jj2)) \/ (LSeg ((Gauge C,((max (max k1,k2),m9) + 1)) * ii1,jj2),((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2)) or x in Ball p9,r )
assume A245:
x in (LSeg ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1),((Gauge C,((max (max k1,k2),m9) + 1)) * ii1,jj2)) \/ (LSeg ((Gauge C,((max (max k1,k2),m9) + 1)) * ii1,jj2),((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2))
;
x in Ball p9,r
then reconsider x9 =
x as
Point of
(TOP-REAL 2) ;
now per cases
( x9 in LSeg ((Upper_Seq C,((max (max k1,k2),m9) + 1)) /. i1),((Gauge C,((max (max k1,k2),m9) + 1)) * ii1,jj2) or x9 in LSeg ((Gauge C,((max (max k1,k2),m9) + 1)) * ii1,jj2),((Lower_Seq C,((max (max k1,k2),m9) + 1)) /. i2) )
by A245, XBOOLE_0:def 3;
end;
hence
x in Ball p9,
r
;
verum
end; hence
Ball p9,
r meets Lower_Arc C
by A147, A168, A179, A186, A189, A194, A207, A211, A213, A215, A244, Th25, XBOOLE_1:63;
verum end; hence
Ball p9,
r meets Lower_Arc C
;
verum end;
then
p in Cl (Lower_Arc C)
by A8, GOBOARD6:96;
then
p in Lower_Arc C
by PRE_TOPC:52;
then
p in (Upper_Arc C) /\ (Lower_Arc C)
by A127, XBOOLE_0:def 4;
then
p in {(W-min C),(E-max C)}
by JORDAN6:65;
then
( p = W-min C or p = E-max C )
by TARSKI:def 2;
hence
contradiction
by A1, A2, EUCLID:56; verum