let C be Simple_closed_curve; :: thesis: 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); :: thesis: ( W-bound C < p `1 & p `1 < E-bound C & p in North_Arc C implies not p in South_Arc C )
reconsider p' = 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
; :: thesis: contradiction
set s = min ((p `1 ) - (W-bound C)),((E-bound C) - (p `1 ));
( W-bound C = (W-bound C) + 0 & p `1 = (p `1 ) + 0 )
;
then
( (p `1 ) - (W-bound C) > 0 & (E-bound C) - (p `1 ) > 0 )
by A1, A2, XREAL_1:22;
then A5:
min ((p `1 ) - (W-bound C)),((E-bound C) - (p `1 )) > 0
by XXREAL_0:15;
now let r be
real number ;
:: thesis: ( 0 < r & r < min ((p `1 ) - (W-bound C)),((E-bound C) - (p `1 )) implies Ball p',r meets Upper_Arc C )reconsider rr =
r as
Real by XREAL_0:def 1;
assume A6:
(
0 < r &
r < min ((p `1 ) - (W-bound C)),
((E-bound C) - (p `1 )) )
;
:: thesis: Ball p',r meets Upper_Arc Cthen A7:
r / 8
> 0
by XREAL_1:141;
then reconsider G =
Ball p',
(r / 8) as
a_neighborhood of
p by GOBOARD6:5;
consider k1 being
Element of
NAT such that A8:
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 A9:
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;
A10:
max k1,
k2 >= k1
by XXREAL_0:25;
set z' =
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
by XXREAL_0:25;
then
(max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (r / 8) >= 1
by A7, XREAL_1:183;
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 m' =
[\(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;
A11:
2
to_power (m' + 1) > 0
by POWER:39;
set N = 2
to_power (m' + 1);
log 2,
((max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (r / 8)) < (m' + 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)) < (m' + 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 (m' + 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 (m' + 1)
by A11, 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 (m' + 1)) * (r / 8)
by A7, XREAL_1:70;
then
max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),
(r / 8) < (2 to_power (m' + 1)) * (r / 8)
by A7, XCMPLX_1:88;
then
(max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (2 to_power (m' + 1)) < ((2 to_power (m' + 1)) * (r / 8)) / (2 to_power (m' + 1))
by A11, XREAL_1:76;
then
(max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (2 to_power (m' + 1)) < ((r / 8) / (2 to_power (m' + 1))) * (2 to_power (m' + 1))
;
then A12:
(max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (2 to_power (m' + 1)) < r / 8
by A11, XCMPLX_1:88;
max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),
(r / 8) >= max ((N-bound C) - (S-bound C)),
((E-bound C) - (W-bound C))
by XXREAL_0:25;
then
(max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (2 to_power (m' + 1)) >= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m' + 1))
by A11, XREAL_1:74;
then A13:
(max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m' + 1)) < r / 8
by A12, XXREAL_0:2;
set m =
(max (max k1,k2),m') + 1;
A14:
len (Gauge C,((max (max k1,k2),m') + 1)) = width (Gauge C,((max (max k1,k2),m') + 1))
by JORDAN8:def 1;
max (max k1,k2),
m' >= max k1,
k2
by XXREAL_0:25;
then
max (max k1,k2),
m' >= k1
by A10, XXREAL_0:2;
then
(max (max k1,k2),m') + 1
> k1
by NAT_1:13;
then
(Upper_Appr C) . ((max (max k1,k2),m') + 1) meets G
by A8;
then
Upper_Arc (L~ (Cage C,((max (max k1,k2),m') + 1))) meets G
by Def1;
then consider p1 being
set such that A15:
p1 in Upper_Arc (L~ (Cage C,((max (max k1,k2),m') + 1)))
and A16:
p1 in G
by XBOOLE_0:3;
reconsider p1 =
p1 as
Point of
(TOP-REAL 2) by A15;
reconsider p1' =
p1 as
Point of
(Euclid 2) by EUCLID:25;
set f =
Upper_Seq C,
((max (max k1,k2),m') + 1);
A17:
Upper_Arc (L~ (Cage C,((max (max k1,k2),m') + 1))) = L~ (Upper_Seq C,((max (max k1,k2),m') + 1))
by JORDAN1G:63;
then consider i1 being
Element of
NAT such that A18:
( 1
<= i1 &
i1 + 1
<= len (Upper_Seq C,((max (max k1,k2),m') + 1)) )
and A19:
p1 in LSeg ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1),
((Upper_Seq C,((max (max k1,k2),m') + 1)) /. (i1 + 1))
by A15, SPPOL_2:14;
reconsider c1 =
(Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1 as
Point of
(Euclid 2) by EUCLID:25;
reconsider c2 =
(Upper_Seq C,((max (max k1,k2),m') + 1)) /. (i1 + 1) as
Point of
(Euclid 2) by EUCLID:25;
A20:
Upper_Seq C,
((max (max k1,k2),m') + 1) is_sequence_on Gauge C,
((max (max k1,k2),m') + 1)
by JORDAN1G:4;
i1 < len (Upper_Seq C,((max (max k1,k2),m') + 1))
by A18, NAT_1:13;
then
i1 in Seg (len (Upper_Seq C,((max (max k1,k2),m') + 1)))
by A18, FINSEQ_1:3;
then A21:
i1 in dom (Upper_Seq C,((max (max k1,k2),m') + 1))
by FINSEQ_1:def 3;
then consider ii1,
jj1 being
Element of
NAT such that A22:
[ii1,jj1] in Indices (Gauge C,((max (max k1,k2),m') + 1))
and A23:
(Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1 = (Gauge C,((max (max k1,k2),m') + 1)) * ii1,
jj1
by A20, GOBOARD1:def 11;
(
N-bound C > (S-bound C) + 0 &
E-bound C > (W-bound C) + 0 )
by TOPREAL5:22, TOPREAL5:23;
then A24:
(
(N-bound C) - (S-bound C) > 0 &
(E-bound C) - (W-bound C) > 0 )
by XREAL_1:22;
A25:
2
|^ (m' + 1) > 0
by A11, POWER:46;
max (max k1,k2),
m' >= m'
by XXREAL_0:25;
then
(max (max k1,k2),m') + 1
> m'
by NAT_1:13;
then
(max (max k1,k2),m') + 1
>= m' + 1
by NAT_1:13;
then
2
|^ ((max (max k1,k2),m') + 1) >= 2
|^ (m' + 1)
by PREPOWER:107;
then A26:
(
((N-bound C) - (S-bound C)) / (2 |^ ((max (max k1,k2),m') + 1)) <= ((N-bound C) - (S-bound C)) / (2 |^ (m' + 1)) &
((E-bound C) - (W-bound C)) / (2 |^ ((max (max k1,k2),m') + 1)) <= ((E-bound C) - (W-bound C)) / (2 |^ (m' + 1)) )
by A24, A25, XREAL_1:120;
(
(N-bound C) - (S-bound C) <= max ((N-bound C) - (S-bound C)),
((E-bound C) - (W-bound C)) &
(E-bound C) - (W-bound C) <= max ((N-bound C) - (S-bound C)),
((E-bound C) - (W-bound C)) )
by XXREAL_0:25;
then
(
((N-bound C) - (S-bound C)) / (2 to_power (m' + 1)) <= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m' + 1)) &
((E-bound C) - (W-bound C)) / (2 to_power (m' + 1)) <= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m' + 1)) )
by A11, XREAL_1:74;
then
(
((N-bound C) - (S-bound C)) / (2 |^ (m' + 1)) <= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m' + 1)) &
((E-bound C) - (W-bound C)) / (2 |^ (m' + 1)) <= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m' + 1)) )
by POWER:46;
then A27:
(
((N-bound C) - (S-bound C)) / (2 |^ ((max (max k1,k2),m') + 1)) <= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m' + 1)) &
((E-bound C) - (W-bound C)) / (2 |^ ((max (max k1,k2),m') + 1)) <= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m' + 1)) )
by A26, XXREAL_0:2;
then
dist ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1),
((Upper_Seq C,((max (max k1,k2),m') + 1)) /. (i1 + 1)) <= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m' + 1))
by A18, A20, Th6;
then
dist ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1),
((Upper_Seq C,((max (max k1,k2),m') + 1)) /. (i1 + 1)) < r / 8
by A13, XXREAL_0:2;
then
dist c1,
c2 < r / 8
by TOPREAL6:def 1;
then A28:
|.(((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) - ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. (i1 + 1))).| < r / 8
by SPPOL_1:62;
|.(p1 - ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1)).| <= |.(((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) - ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. (i1 + 1))).|
by A19, JGRAPH_1:53;
then A29:
|.(p1 - ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1)).| < r / 8
by A28, XXREAL_0:2;
dist p1',
p' < r / 8
by A16, METRIC_1:12;
then
|.(p - p1).| < r / 8
by SPPOL_1:62;
then A30:
|.(p - p1).| + |.(p1 - ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1)).| < (r / (2 * 4)) + (r / (2 * 4))
by A29, XREAL_1:10;
|.(p - ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1)).| <= |.(p - p1).| + |.(p1 - ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1)).|
by TOPRNS_1:35;
then A31:
|.(p - ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1)).| < r / 4
by A30, XXREAL_0:2;
then A32:
dist p',
c1 < r / 4
by SPPOL_1:62;
then A33:
(Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1 in Ball p',
(r / 4)
by METRIC_1:12;
A34:
(Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1 in Upper_Arc (L~ (Cage C,((max (max k1,k2),m') + 1)))
by A17, A21, SPPOL_2:48;
A35:
max k1,
k2 >= k2
by XXREAL_0:25;
max (max k1,k2),
m' >= max k1,
k2
by XXREAL_0:25;
then
max (max k1,k2),
m' >= k2
by A35, XXREAL_0:2;
then
(max (max k1,k2),m') + 1
> k2
by NAT_1:13;
then
(Lower_Appr C) . ((max (max k1,k2),m') + 1) meets G
by A9;
then
Lower_Arc (L~ (Cage C,((max (max k1,k2),m') + 1))) meets G
by Def2;
then consider p2 being
set such that A36:
p2 in Lower_Arc (L~ (Cage C,((max (max k1,k2),m') + 1)))
and A37:
p2 in G
by XBOOLE_0:3;
reconsider p2 =
p2 as
Point of
(TOP-REAL 2) by A36;
reconsider p2' =
p2 as
Point of
(Euclid 2) by EUCLID:25;
set g =
Lower_Seq C,
((max (max k1,k2),m') + 1);
A38:
Lower_Arc (L~ (Cage C,((max (max k1,k2),m') + 1))) = L~ (Lower_Seq C,((max (max k1,k2),m') + 1))
by JORDAN1G:64;
then consider i2 being
Element of
NAT such that A39:
( 1
<= i2 &
i2 + 1
<= len (Lower_Seq C,((max (max k1,k2),m') + 1)) )
and A40:
p2 in LSeg ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2),
((Lower_Seq C,((max (max k1,k2),m') + 1)) /. (i2 + 1))
by A36, SPPOL_2:14;
reconsider d1 =
(Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2 as
Point of
(Euclid 2) by EUCLID:25;
reconsider d2 =
(Lower_Seq C,((max (max k1,k2),m') + 1)) /. (i2 + 1) as
Point of
(Euclid 2) by EUCLID:25;
A41:
Lower_Seq C,
((max (max k1,k2),m') + 1) is_sequence_on Gauge C,
((max (max k1,k2),m') + 1)
by JORDAN1G:5;
i2 < len (Lower_Seq C,((max (max k1,k2),m') + 1))
by A39, NAT_1:13;
then
i2 in Seg (len (Lower_Seq C,((max (max k1,k2),m') + 1)))
by A39, FINSEQ_1:3;
then A42:
i2 in dom (Lower_Seq C,((max (max k1,k2),m') + 1))
by FINSEQ_1:def 3;
then consider ii2,
jj2 being
Element of
NAT such that A43:
[ii2,jj2] in Indices (Gauge C,((max (max k1,k2),m') + 1))
and A44:
(Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2 = (Gauge C,((max (max k1,k2),m') + 1)) * ii2,
jj2
by A41, GOBOARD1:def 11;
dist ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2),
((Lower_Seq C,((max (max k1,k2),m') + 1)) /. (i2 + 1)) <= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m' + 1))
by A27, A39, A41, Th6;
then
dist ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2),
((Lower_Seq C,((max (max k1,k2),m') + 1)) /. (i2 + 1)) < r / 8
by A13, XXREAL_0:2;
then
dist d1,
d2 < r / 8
by TOPREAL6:def 1;
then A45:
|.(((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) - ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. (i2 + 1))).| < r / 8
by SPPOL_1:62;
|.(p2 - ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2)).| <= |.(((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) - ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. (i2 + 1))).|
by A40, JGRAPH_1:53;
then A46:
|.(p2 - ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2)).| < r / 8
by A45, XXREAL_0:2;
dist p2',
p' < r / 8
by A37, METRIC_1:12;
then
|.(p - p2).| < r / 8
by SPPOL_1:62;
then A47:
|.(p - p2).| + |.(p2 - ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2)).| < (r / (2 * 4)) + (r / (2 * 4))
by A46, XREAL_1:10;
|.(p - ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2)).| <= |.(p - p2).| + |.(p2 - ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2)).|
by TOPRNS_1:35;
then A48:
|.(p - ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2)).| < r / 4
by A47, XXREAL_0:2;
then A49:
dist p',
d1 < r / 4
by SPPOL_1:62;
then A50:
(Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2 in Ball p',
(r / 4)
by METRIC_1:12;
A51:
(Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2 in Lower_Arc (L~ (Cage C,((max (max k1,k2),m') + 1)))
by A38, A42, SPPOL_2:48;
set Gij =
(Gauge C,((max (max k1,k2),m') + 1)) * ii2,
jj1;
set Gji =
(Gauge C,((max (max k1,k2),m') + 1)) * ii1,
jj2;
reconsider Gij' =
(Gauge C,((max (max k1,k2),m') + 1)) * ii2,
jj1,
Gji' =
(Gauge C,((max (max k1,k2),m') + 1)) * ii1,
jj2 as
Point of
(Euclid 2) by EUCLID:25;
A52:
( 1
<= ii1 &
ii1 <= len (Gauge C,((max (max k1,k2),m') + 1)) & 1
<= jj1 &
jj1 <= width (Gauge C,((max (max k1,k2),m') + 1)) )
by A22, MATRIX_1:39;
A53:
( 1
<= ii2 &
ii2 <= len (Gauge C,((max (max k1,k2),m') + 1)) & 1
<= jj2 &
jj2 <= width (Gauge C,((max (max k1,k2),m') + 1)) )
by A43, MATRIX_1:39;
(
len (Upper_Seq C,((max (max k1,k2),m') + 1)) >= 3 &
len (Lower_Seq C,((max (max k1,k2),m') + 1)) >= 3 )
by JORDAN1E:19;
then
(
len (Upper_Seq C,((max (max k1,k2),m') + 1)) >= 1 &
len (Lower_Seq C,((max (max k1,k2),m') + 1)) >= 1 )
by XXREAL_0:2;
then
(
len (Upper_Seq C,((max (max k1,k2),m') + 1)) in Seg (len (Upper_Seq C,((max (max k1,k2),m') + 1))) &
len (Lower_Seq C,((max (max k1,k2),m') + 1)) in Seg (len (Lower_Seq C,((max (max k1,k2),m') + 1))) )
by FINSEQ_1:3;
then A54:
(
len (Upper_Seq C,((max (max k1,k2),m') + 1)) in dom (Upper_Seq C,((max (max k1,k2),m') + 1)) &
len (Lower_Seq C,((max (max k1,k2),m') + 1)) in dom (Lower_Seq C,((max (max k1,k2),m') + 1)) )
by FINSEQ_1:def 3;
A55:
r / 4
< r
by A6, XREAL_1:225;
A56:
r / 2
< r
by A6, XREAL_1:218;
A57:
(
min ((p `1 ) - (W-bound C)),
((E-bound C) - (p `1 )) <= (p `1 ) - (W-bound C) &
min ((p `1 ) - (W-bound C)),
((E-bound C) - (p `1 )) <= (E-bound C) - (p `1 ) )
by XXREAL_0:17;
A58:
now assume
1
>= ii1
;
:: thesis: contradictionthen A59:
ii1 = 1
by A52, XXREAL_0:1;
dist p',
c1 < r
by A32, A55, XXREAL_0:2;
then
dist p',
c1 < min ((p `1 ) - (W-bound C)),
((E-bound C) - (p `1 ))
by A6, XXREAL_0:2;
then A60:
dist p',
c1 < (p `1 ) - (W-bound C)
by A57, XXREAL_0:2;
A61:
(p `1 ) - (((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `1 ) <= abs ((p `1 ) - (((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `1 ))
by ABSVALUE:11;
abs ((p `1 ) - (((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `1 )) <= |.(p - ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1)).|
by JGRAPH_1:51;
then
(p `1 ) - (((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `1 ) <= |.(p - ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1)).|
by A61, XXREAL_0:2;
then
(p `1 ) - (W-bound (L~ (Cage C,((max (max k1,k2),m') + 1)))) <= |.(p - ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1)).|
by A14, A23, A52, A59, JORDAN1A:94;
then
(p `1 ) - (W-bound (L~ (Cage C,((max (max k1,k2),m') + 1)))) <= dist p',
c1
by SPPOL_1:62;
then
(p `1 ) - (W-bound (L~ (Cage C,((max (max k1,k2),m') + 1)))) < (p `1 ) - (W-bound C)
by A60, XXREAL_0:2;
then
W-bound (L~ (Cage C,((max (max k1,k2),m') + 1))) > W-bound C
by XREAL_1:15;
hence
contradiction
by Th12;
:: thesis: verum end; A62:
now assume
ii1 >= len (Gauge C,((max (max k1,k2),m') + 1))
;
:: thesis: contradictionthen A63:
ii1 = len (Gauge C,((max (max k1,k2),m') + 1))
by A52, XXREAL_0:1;
((Gauge C,((max (max k1,k2),m') + 1)) * (len (Gauge C,((max (max k1,k2),m') + 1))),jj1) `1 = E-bound (L~ (Cage C,((max (max k1,k2),m') + 1)))
by A14, A52, JORDAN1A:92;
then (Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1 =
E-max (L~ (Cage C,((max (max k1,k2),m') + 1)))
by A17, A21, A23, A63, JORDAN1J:46, SPPOL_2:48
.=
(Upper_Seq C,((max (max k1,k2),m') + 1)) /. (len (Upper_Seq C,((max (max k1,k2),m') + 1)))
by JORDAN1F:7
;
then
i1 = len (Upper_Seq C,((max (max k1,k2),m') + 1))
by A21, A54, PARTFUN2:17;
hence
contradiction
by A18, NAT_1:13;
:: thesis: verum end; A64:
now assume
ii2 <= 1
;
:: thesis: contradictionthen A65:
ii2 = 1
by A53, XXREAL_0:1;
((Gauge C,((max (max k1,k2),m') + 1)) * 1,jj2) `1 = W-bound (L~ (Cage C,((max (max k1,k2),m') + 1)))
by A14, A53, JORDAN1A:94;
then (Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2 =
W-min (L~ (Cage C,((max (max k1,k2),m') + 1)))
by A38, A42, A44, A65, JORDAN1J:47, SPPOL_2:48
.=
(Lower_Seq C,((max (max k1,k2),m') + 1)) /. (len (Lower_Seq C,((max (max k1,k2),m') + 1)))
by JORDAN1F:8
;
then
i2 = len (Lower_Seq C,((max (max k1,k2),m') + 1))
by A42, A54, PARTFUN2:17;
hence
contradiction
by A39, NAT_1:13;
:: thesis: verum end; A66:
now assume
ii2 >= len (Gauge C,((max (max k1,k2),m') + 1))
;
:: thesis: contradictionthen A67:
ii2 = len (Gauge C,((max (max k1,k2),m') + 1))
by A53, XXREAL_0:1;
dist p',
d1 < r
by A49, A55, XXREAL_0:2;
then
dist p',
d1 < min ((p `1 ) - (W-bound C)),
((E-bound C) - (p `1 ))
by A6, XXREAL_0:2;
then A68:
dist p',
d1 < (E-bound C) - (p `1 )
by A57, XXREAL_0:2;
A69:
(((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `1 ) - (p `1 ) <= abs ((((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `1 ) - (p `1 ))
by ABSVALUE:11;
abs ((((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `1 ) - (p `1 )) <= |.(((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) - p).|
by JGRAPH_1:51;
then
abs ((((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `1 ) - (p `1 )) <= |.(p - ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2)).|
by TOPRNS_1:28;
then
(((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `1 ) - (p `1 ) <= |.(p - ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2)).|
by A69, XXREAL_0:2;
then
(E-bound (L~ (Cage C,((max (max k1,k2),m') + 1)))) - (p `1 ) <= |.(p - ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2)).|
by A14, A44, A53, A67, JORDAN1A:92;
then
(E-bound (L~ (Cage C,((max (max k1,k2),m') + 1)))) - (p `1 ) <= dist p',
d1
by SPPOL_1:62;
then
(E-bound (L~ (Cage C,((max (max k1,k2),m') + 1)))) - (p `1 ) < (E-bound C) - (p `1 )
by A68, XXREAL_0:2;
then
E-bound (L~ (Cage C,((max (max k1,k2),m') + 1))) < E-bound C
by XREAL_1:15;
hence
contradiction
by Th10;
:: thesis: verum end; A70:
Ball p',
(rr / 4) c= Ball p',
rr
by A55, PCOMPS_1:1;
A71:
((Gauge C,((max (max k1,k2),m') + 1)) * ii2,jj1) `1 =
((Gauge C,((max (max k1,k2),m') + 1)) * ii2,1) `1
by A52, A53, GOBOARD5:3
.=
((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `1
by A44, A53, GOBOARD5:3
;
A72:
((Gauge C,((max (max k1,k2),m') + 1)) * ii2,jj1) `2 =
((Gauge C,((max (max k1,k2),m') + 1)) * 1,jj1) `2
by A52, A53, GOBOARD5:2
.=
((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `2
by A23, A52, GOBOARD5:2
;
A73:
((Gauge C,((max (max k1,k2),m') + 1)) * ii1,jj2) `1 =
((Gauge C,((max (max k1,k2),m') + 1)) * ii1,1) `1
by A52, A53, GOBOARD5:3
.=
((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `1
by A23, A52, GOBOARD5:3
;
A74:
((Gauge C,((max (max k1,k2),m') + 1)) * ii1,jj2) `2 =
((Gauge C,((max (max k1,k2),m') + 1)) * 1,jj2) `2
by A52, A53, GOBOARD5:2
.=
((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `2
by A44, A53, GOBOARD5:2
;
(
abs ((((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `1 ) - (p `1 )) <= |.(((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) - p).| &
abs ((((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `2 ) - (p `2 )) <= |.(((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) - p).| )
by JGRAPH_1:51;
then
(
abs ((((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `1 ) - (p `1 )) <= |.(p - ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2)).| &
abs ((((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `2 ) - (p `2 )) <= |.(p - ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1)).| )
by TOPRNS_1:28;
then
(
abs ((((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `1 ) - (p `1 )) <= r / 4 &
abs ((((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `2 ) - (p `2 )) <= r / 4 )
by A31, A48, XXREAL_0:2;
then
(abs ((((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `1 ) - (p `1 ))) + (abs ((((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `2 ) - (p `2 ))) <= (r / (2 * 2)) + (r / (2 * 2))
by XREAL_1:9;
then A75:
(abs ((((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `1 ) - (p `1 ))) + (abs ((((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `2 ) - (p `2 ))) < r
by A56, XXREAL_0:2;
(
abs ((((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `1 ) - (p `1 )) <= |.(((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) - p).| &
abs ((((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `2 ) - (p `2 )) <= |.(((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) - p).| )
by JGRAPH_1:51;
then
(
abs ((((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `1 ) - (p `1 )) <= |.(p - ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1)).| &
abs ((((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `2 ) - (p `2 )) <= |.(p - ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2)).| )
by TOPRNS_1:28;
then
(
abs ((((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `1 ) - (p `1 )) <= r / 4 &
abs ((((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `2 ) - (p `2 )) <= r / 4 )
by A31, A48, XXREAL_0:2;
then
(abs ((((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `1 ) - (p `1 ))) + (abs ((((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `2 ) - (p `2 ))) <= (r / (2 * 2)) + (r / (2 * 2))
by XREAL_1:9;
then A76:
(abs ((((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `1 ) - (p `1 ))) + (abs ((((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `2 ) - (p `2 ))) < r
by A56, XXREAL_0:2;
|.(((Gauge C,((max (max k1,k2),m') + 1)) * ii2,jj1) - p).| <= (abs ((((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `1 ) - (p `1 ))) + (abs ((((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `2 ) - (p `2 )))
by A71, A72, JGRAPH_1:49;
then
|.(((Gauge C,((max (max k1,k2),m') + 1)) * ii2,jj1) - p).| < r
by A75, XXREAL_0:2;
then
dist Gij',
p' < r
by SPPOL_1:62;
then A77:
(Gauge C,((max (max k1,k2),m') + 1)) * ii2,
jj1 in Ball p',
r
by METRIC_1:12;
|.(((Gauge C,((max (max k1,k2),m') + 1)) * ii1,jj2) - p).| <= (abs ((((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `1 ) - (p `1 ))) + (abs ((((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `2 ) - (p `2 )))
by A73, A74, JGRAPH_1:49;
then
|.(((Gauge C,((max (max k1,k2),m') + 1)) * ii1,jj2) - p).| < r
by A76, XXREAL_0:2;
then
dist Gji',
p' < r
by SPPOL_1:62;
then A78:
(Gauge C,((max (max k1,k2),m') + 1)) * ii1,
jj2 in Ball p',
r
by METRIC_1:12;
A79:
LSeg ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2),
((Gauge C,((max (max k1,k2),m') + 1)) * ii2,jj1) c= Ball p',
rr
by A50, A70, A77, TOPREAL3:28;
A80:
LSeg ((Gauge C,((max (max k1,k2),m') + 1)) * ii2,jj1),
((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) c= Ball p',
rr
by A33, A70, A77, TOPREAL3:28;
A81:
LSeg ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2),
((Gauge C,((max (max k1,k2),m') + 1)) * ii1,jj2) c= Ball p',
rr
by A50, A70, A78, TOPREAL3:28;
A82:
LSeg ((Gauge C,((max (max k1,k2),m') + 1)) * ii1,jj2),
((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) c= Ball p',
rr
by A33, A70, A78, TOPREAL3:28;
now per cases
( jj2 <= jj1 or jj1 < jj2 )
;
suppose A83:
jj2 <= jj1
;
:: thesis: Ball p',r meets Upper_Arc C
(LSeg ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2),((Gauge C,((max (max k1,k2),m') + 1)) * ii2,jj1)) \/ (LSeg ((Gauge C,((max (max k1,k2),m') + 1)) * ii2,jj1),((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1)) c= Ball p',
r
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in (LSeg ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2),((Gauge C,((max (max k1,k2),m') + 1)) * ii2,jj1)) \/ (LSeg ((Gauge C,((max (max k1,k2),m') + 1)) * ii2,jj1),((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1)) or x in Ball p',r )
assume A84:
x in (LSeg ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2),((Gauge C,((max (max k1,k2),m') + 1)) * ii2,jj1)) \/ (LSeg ((Gauge C,((max (max k1,k2),m') + 1)) * ii2,jj1),((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1))
;
:: thesis: x in Ball p',r
then reconsider x' =
x as
Point of
(TOP-REAL 2) ;
now per cases
( x' in LSeg ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2),((Gauge C,((max (max k1,k2),m') + 1)) * ii2,jj1) or x' in LSeg ((Gauge C,((max (max k1,k2),m') + 1)) * ii2,jj1),((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) )
by A84, XBOOLE_0:def 3;
end;
hence
x in Ball p',
r
;
:: thesis: verum
end; hence
Ball p',
r meets Upper_Arc C
by A23, A34, A44, A51, A52, A53, A58, A62, A64, A66, A83, JORDAN15:50, XBOOLE_1:63;
:: thesis: verum end; suppose A85:
jj1 < jj2
;
:: thesis: Ball p',r meets Upper_Arc C
(LSeg ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1),((Gauge C,((max (max k1,k2),m') + 1)) * ii1,jj2)) \/ (LSeg ((Gauge C,((max (max k1,k2),m') + 1)) * ii1,jj2),((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2)) c= Ball p',
r
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in (LSeg ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1),((Gauge C,((max (max k1,k2),m') + 1)) * ii1,jj2)) \/ (LSeg ((Gauge C,((max (max k1,k2),m') + 1)) * ii1,jj2),((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2)) or x in Ball p',r )
assume A86:
x in (LSeg ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1),((Gauge C,((max (max k1,k2),m') + 1)) * ii1,jj2)) \/ (LSeg ((Gauge C,((max (max k1,k2),m') + 1)) * ii1,jj2),((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2))
;
:: thesis: x in Ball p',r
then reconsider x' =
x as
Point of
(TOP-REAL 2) ;
now per cases
( x' in LSeg ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1),((Gauge C,((max (max k1,k2),m') + 1)) * ii1,jj2) or x' in LSeg ((Gauge C,((max (max k1,k2),m') + 1)) * ii1,jj2),((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) )
by A86, XBOOLE_0:def 3;
end;
hence
x in Ball p',
r
;
:: thesis: verum
end; hence
Ball p',
r meets Upper_Arc C
by A23, A34, A44, A51, A52, A53, A58, A62, A64, A66, A85, Th26, XBOOLE_1:63;
:: thesis: verum end; hence
Ball p',
r meets Upper_Arc C
;
:: thesis: verum end;
then
p in Cl (Upper_Arc C)
by A5, GOBOARD6:96;
then A87:
p in Upper_Arc C
by PRE_TOPC:52;
now let r be
real number ;
:: thesis: ( 0 < r & r < min ((p `1 ) - (W-bound C)),((E-bound C) - (p `1 )) implies Ball p',r meets Lower_Arc C )reconsider rr =
r as
Real by XREAL_0:def 1;
assume A88:
(
0 < r &
r < min ((p `1 ) - (W-bound C)),
((E-bound C) - (p `1 )) )
;
:: thesis: Ball p',r meets Lower_Arc Cthen A89:
r / 8
> 0
by XREAL_1:141;
then reconsider G =
Ball p',
(r / 8) as
a_neighborhood of
p by GOBOARD6:5;
consider k1 being
Element of
NAT such that A90:
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 A91:
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;
A92:
max k1,
k2 >= k1
by XXREAL_0:25;
set z' =
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
by XXREAL_0:25;
then
(max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (r / 8) >= 1
by A89, XREAL_1:183;
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 m' =
[\(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;
A93:
2
to_power (m' + 1) > 0
by POWER:39;
set N = 2
to_power (m' + 1);
log 2,
((max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (r / 8)) < (m' + 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)) < (m' + 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 (m' + 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 (m' + 1)
by A93, 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 (m' + 1)) * (r / 8)
by A89, XREAL_1:70;
then
max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),
(r / 8) < (2 to_power (m' + 1)) * (r / 8)
by A89, XCMPLX_1:88;
then
(max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (2 to_power (m' + 1)) < ((2 to_power (m' + 1)) * (r / 8)) / (2 to_power (m' + 1))
by A93, XREAL_1:76;
then
(max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (2 to_power (m' + 1)) < ((r / 8) / (2 to_power (m' + 1))) * (2 to_power (m' + 1))
;
then A94:
(max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (2 to_power (m' + 1)) < r / 8
by A93, XCMPLX_1:88;
max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),
(r / 8) >= max ((N-bound C) - (S-bound C)),
((E-bound C) - (W-bound C))
by XXREAL_0:25;
then
(max (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))),(r / 8)) / (2 to_power (m' + 1)) >= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m' + 1))
by A93, XREAL_1:74;
then A95:
(max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m' + 1)) < r / 8
by A94, XXREAL_0:2;
set m =
(max (max k1,k2),m') + 1;
A96:
len (Gauge C,((max (max k1,k2),m') + 1)) = width (Gauge C,((max (max k1,k2),m') + 1))
by JORDAN8:def 1;
max (max k1,k2),
m' >= max k1,
k2
by XXREAL_0:25;
then
max (max k1,k2),
m' >= k1
by A92, XXREAL_0:2;
then
(max (max k1,k2),m') + 1
> k1
by NAT_1:13;
then
(Upper_Appr C) . ((max (max k1,k2),m') + 1) meets G
by A90;
then
Upper_Arc (L~ (Cage C,((max (max k1,k2),m') + 1))) meets G
by Def1;
then consider p1 being
set such that A97:
p1 in Upper_Arc (L~ (Cage C,((max (max k1,k2),m') + 1)))
and A98:
p1 in G
by XBOOLE_0:3;
reconsider p1 =
p1 as
Point of
(TOP-REAL 2) by A97;
reconsider p1' =
p1 as
Point of
(Euclid 2) by EUCLID:25;
set f =
Upper_Seq C,
((max (max k1,k2),m') + 1);
A99:
Upper_Arc (L~ (Cage C,((max (max k1,k2),m') + 1))) = L~ (Upper_Seq C,((max (max k1,k2),m') + 1))
by JORDAN1G:63;
then consider i1 being
Element of
NAT such that A100:
( 1
<= i1 &
i1 + 1
<= len (Upper_Seq C,((max (max k1,k2),m') + 1)) )
and A101:
p1 in LSeg ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1),
((Upper_Seq C,((max (max k1,k2),m') + 1)) /. (i1 + 1))
by A97, SPPOL_2:14;
reconsider c1 =
(Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1 as
Point of
(Euclid 2) by EUCLID:25;
reconsider c2 =
(Upper_Seq C,((max (max k1,k2),m') + 1)) /. (i1 + 1) as
Point of
(Euclid 2) by EUCLID:25;
A102:
Upper_Seq C,
((max (max k1,k2),m') + 1) is_sequence_on Gauge C,
((max (max k1,k2),m') + 1)
by JORDAN1G:4;
i1 < len (Upper_Seq C,((max (max k1,k2),m') + 1))
by A100, NAT_1:13;
then
i1 in Seg (len (Upper_Seq C,((max (max k1,k2),m') + 1)))
by A100, FINSEQ_1:3;
then A103:
i1 in dom (Upper_Seq C,((max (max k1,k2),m') + 1))
by FINSEQ_1:def 3;
then consider ii1,
jj1 being
Element of
NAT such that A104:
[ii1,jj1] in Indices (Gauge C,((max (max k1,k2),m') + 1))
and A105:
(Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1 = (Gauge C,((max (max k1,k2),m') + 1)) * ii1,
jj1
by A102, GOBOARD1:def 11;
(
N-bound C > (S-bound C) + 0 &
E-bound C > (W-bound C) + 0 )
by TOPREAL5:22, TOPREAL5:23;
then A106:
(
(N-bound C) - (S-bound C) > 0 &
(E-bound C) - (W-bound C) > 0 )
by XREAL_1:22;
A107:
2
|^ (m' + 1) > 0
by A93, POWER:46;
max (max k1,k2),
m' >= m'
by XXREAL_0:25;
then
(max (max k1,k2),m') + 1
> m'
by NAT_1:13;
then
(max (max k1,k2),m') + 1
>= m' + 1
by NAT_1:13;
then
2
|^ ((max (max k1,k2),m') + 1) >= 2
|^ (m' + 1)
by PREPOWER:107;
then A108:
(
((N-bound C) - (S-bound C)) / (2 |^ ((max (max k1,k2),m') + 1)) <= ((N-bound C) - (S-bound C)) / (2 |^ (m' + 1)) &
((E-bound C) - (W-bound C)) / (2 |^ ((max (max k1,k2),m') + 1)) <= ((E-bound C) - (W-bound C)) / (2 |^ (m' + 1)) )
by A106, A107, XREAL_1:120;
(
(N-bound C) - (S-bound C) <= max ((N-bound C) - (S-bound C)),
((E-bound C) - (W-bound C)) &
(E-bound C) - (W-bound C) <= max ((N-bound C) - (S-bound C)),
((E-bound C) - (W-bound C)) )
by XXREAL_0:25;
then
(
((N-bound C) - (S-bound C)) / (2 to_power (m' + 1)) <= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m' + 1)) &
((E-bound C) - (W-bound C)) / (2 to_power (m' + 1)) <= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m' + 1)) )
by A93, XREAL_1:74;
then
(
((N-bound C) - (S-bound C)) / (2 |^ (m' + 1)) <= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m' + 1)) &
((E-bound C) - (W-bound C)) / (2 |^ (m' + 1)) <= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m' + 1)) )
by POWER:46;
then A109:
(
((N-bound C) - (S-bound C)) / (2 |^ ((max (max k1,k2),m') + 1)) <= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m' + 1)) &
((E-bound C) - (W-bound C)) / (2 |^ ((max (max k1,k2),m') + 1)) <= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m' + 1)) )
by A108, XXREAL_0:2;
then
dist ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1),
((Upper_Seq C,((max (max k1,k2),m') + 1)) /. (i1 + 1)) <= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m' + 1))
by A100, A102, Th6;
then
dist ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1),
((Upper_Seq C,((max (max k1,k2),m') + 1)) /. (i1 + 1)) < r / 8
by A95, XXREAL_0:2;
then
dist c1,
c2 < r / 8
by TOPREAL6:def 1;
then A110:
|.(((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) - ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. (i1 + 1))).| < r / 8
by SPPOL_1:62;
|.(p1 - ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1)).| <= |.(((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) - ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. (i1 + 1))).|
by A101, JGRAPH_1:53;
then A111:
|.(p1 - ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1)).| < r / 8
by A110, XXREAL_0:2;
dist p1',
p' < r / 8
by A98, METRIC_1:12;
then
|.(p - p1).| < r / 8
by SPPOL_1:62;
then A112:
|.(p - p1).| + |.(p1 - ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1)).| < (r / (2 * 4)) + (r / (2 * 4))
by A111, XREAL_1:10;
|.(p - ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1)).| <= |.(p - p1).| + |.(p1 - ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1)).|
by TOPRNS_1:35;
then A113:
|.(p - ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1)).| < r / 4
by A112, XXREAL_0:2;
then A114:
dist p',
c1 < r / 4
by SPPOL_1:62;
then A115:
(Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1 in Ball p',
(r / 4)
by METRIC_1:12;
A116:
(Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1 in Upper_Arc (L~ (Cage C,((max (max k1,k2),m') + 1)))
by A99, A103, SPPOL_2:48;
A117:
max k1,
k2 >= k2
by XXREAL_0:25;
max (max k1,k2),
m' >= max k1,
k2
by XXREAL_0:25;
then
max (max k1,k2),
m' >= k2
by A117, XXREAL_0:2;
then
(max (max k1,k2),m') + 1
> k2
by NAT_1:13;
then
(Lower_Appr C) . ((max (max k1,k2),m') + 1) meets G
by A91;
then
Lower_Arc (L~ (Cage C,((max (max k1,k2),m') + 1))) meets G
by Def2;
then consider p2 being
set such that A118:
p2 in Lower_Arc (L~ (Cage C,((max (max k1,k2),m') + 1)))
and A119:
p2 in G
by XBOOLE_0:3;
reconsider p2 =
p2 as
Point of
(TOP-REAL 2) by A118;
reconsider p2' =
p2 as
Point of
(Euclid 2) by EUCLID:25;
set g =
Lower_Seq C,
((max (max k1,k2),m') + 1);
A120:
Lower_Arc (L~ (Cage C,((max (max k1,k2),m') + 1))) = L~ (Lower_Seq C,((max (max k1,k2),m') + 1))
by JORDAN1G:64;
then consider i2 being
Element of
NAT such that A121:
( 1
<= i2 &
i2 + 1
<= len (Lower_Seq C,((max (max k1,k2),m') + 1)) )
and A122:
p2 in LSeg ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2),
((Lower_Seq C,((max (max k1,k2),m') + 1)) /. (i2 + 1))
by A118, SPPOL_2:14;
reconsider d1 =
(Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2 as
Point of
(Euclid 2) by EUCLID:25;
reconsider d2 =
(Lower_Seq C,((max (max k1,k2),m') + 1)) /. (i2 + 1) as
Point of
(Euclid 2) by EUCLID:25;
A123:
Lower_Seq C,
((max (max k1,k2),m') + 1) is_sequence_on Gauge C,
((max (max k1,k2),m') + 1)
by JORDAN1G:5;
i2 < len (Lower_Seq C,((max (max k1,k2),m') + 1))
by A121, NAT_1:13;
then
i2 in Seg (len (Lower_Seq C,((max (max k1,k2),m') + 1)))
by A121, FINSEQ_1:3;
then A124:
i2 in dom (Lower_Seq C,((max (max k1,k2),m') + 1))
by FINSEQ_1:def 3;
then consider ii2,
jj2 being
Element of
NAT such that A125:
[ii2,jj2] in Indices (Gauge C,((max (max k1,k2),m') + 1))
and A126:
(Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2 = (Gauge C,((max (max k1,k2),m') + 1)) * ii2,
jj2
by A123, GOBOARD1:def 11;
dist ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2),
((Lower_Seq C,((max (max k1,k2),m') + 1)) /. (i2 + 1)) <= (max ((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C))) / (2 to_power (m' + 1))
by A109, A121, A123, Th6;
then
dist ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2),
((Lower_Seq C,((max (max k1,k2),m') + 1)) /. (i2 + 1)) < r / 8
by A95, XXREAL_0:2;
then
dist d1,
d2 < r / 8
by TOPREAL6:def 1;
then A127:
|.(((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) - ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. (i2 + 1))).| < r / 8
by SPPOL_1:62;
|.(p2 - ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2)).| <= |.(((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) - ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. (i2 + 1))).|
by A122, JGRAPH_1:53;
then A128:
|.(p2 - ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2)).| < r / 8
by A127, XXREAL_0:2;
dist p2',
p' < r / 8
by A119, METRIC_1:12;
then
|.(p - p2).| < r / 8
by SPPOL_1:62;
then A129:
|.(p - p2).| + |.(p2 - ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2)).| < (r / (2 * 4)) + (r / (2 * 4))
by A128, XREAL_1:10;
|.(p - ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2)).| <= |.(p - p2).| + |.(p2 - ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2)).|
by TOPRNS_1:35;
then A130:
|.(p - ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2)).| < r / 4
by A129, XXREAL_0:2;
then A131:
dist p',
d1 < r / 4
by SPPOL_1:62;
then A132:
(Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2 in Ball p',
(r / 4)
by METRIC_1:12;
A133:
(Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2 in Lower_Arc (L~ (Cage C,((max (max k1,k2),m') + 1)))
by A120, A124, SPPOL_2:48;
set Gij =
(Gauge C,((max (max k1,k2),m') + 1)) * ii2,
jj1;
set Gji =
(Gauge C,((max (max k1,k2),m') + 1)) * ii1,
jj2;
reconsider Gij' =
(Gauge C,((max (max k1,k2),m') + 1)) * ii2,
jj1,
Gji' =
(Gauge C,((max (max k1,k2),m') + 1)) * ii1,
jj2 as
Point of
(Euclid 2) by EUCLID:25;
A134:
( 1
<= ii1 &
ii1 <= len (Gauge C,((max (max k1,k2),m') + 1)) & 1
<= jj1 &
jj1 <= width (Gauge C,((max (max k1,k2),m') + 1)) )
by A104, MATRIX_1:39;
A135:
( 1
<= ii2 &
ii2 <= len (Gauge C,((max (max k1,k2),m') + 1)) & 1
<= jj2 &
jj2 <= width (Gauge C,((max (max k1,k2),m') + 1)) )
by A125, MATRIX_1:39;
(
len (Upper_Seq C,((max (max k1,k2),m') + 1)) >= 3 &
len (Lower_Seq C,((max (max k1,k2),m') + 1)) >= 3 )
by JORDAN1E:19;
then
(
len (Upper_Seq C,((max (max k1,k2),m') + 1)) >= 1 &
len (Lower_Seq C,((max (max k1,k2),m') + 1)) >= 1 )
by XXREAL_0:2;
then
(
len (Upper_Seq C,((max (max k1,k2),m') + 1)) in Seg (len (Upper_Seq C,((max (max k1,k2),m') + 1))) &
len (Lower_Seq C,((max (max k1,k2),m') + 1)) in Seg (len (Lower_Seq C,((max (max k1,k2),m') + 1))) )
by FINSEQ_1:3;
then A136:
(
len (Upper_Seq C,((max (max k1,k2),m') + 1)) in dom (Upper_Seq C,((max (max k1,k2),m') + 1)) &
len (Lower_Seq C,((max (max k1,k2),m') + 1)) in dom (Lower_Seq C,((max (max k1,k2),m') + 1)) )
by FINSEQ_1:def 3;
A137:
r / 4
< r
by A88, XREAL_1:225;
A138:
r / 2
< r
by A88, XREAL_1:218;
A139:
(
min ((p `1 ) - (W-bound C)),
((E-bound C) - (p `1 )) <= (p `1 ) - (W-bound C) &
min ((p `1 ) - (W-bound C)),
((E-bound C) - (p `1 )) <= (E-bound C) - (p `1 ) )
by XXREAL_0:17;
A140:
now assume
1
>= ii1
;
:: thesis: contradictionthen A141:
ii1 = 1
by A134, XXREAL_0:1;
dist p',
c1 < r
by A114, A137, XXREAL_0:2;
then
dist p',
c1 < min ((p `1 ) - (W-bound C)),
((E-bound C) - (p `1 ))
by A88, XXREAL_0:2;
then A142:
dist p',
c1 < (p `1 ) - (W-bound C)
by A139, XXREAL_0:2;
A143:
(p `1 ) - (((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `1 ) <= abs ((p `1 ) - (((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `1 ))
by ABSVALUE:11;
abs ((p `1 ) - (((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `1 )) <= |.(p - ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1)).|
by JGRAPH_1:51;
then
(p `1 ) - (((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `1 ) <= |.(p - ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1)).|
by A143, XXREAL_0:2;
then
(p `1 ) - (W-bound (L~ (Cage C,((max (max k1,k2),m') + 1)))) <= |.(p - ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1)).|
by A96, A105, A134, A141, JORDAN1A:94;
then
(p `1 ) - (W-bound (L~ (Cage C,((max (max k1,k2),m') + 1)))) <= dist p',
c1
by SPPOL_1:62;
then
(p `1 ) - (W-bound (L~ (Cage C,((max (max k1,k2),m') + 1)))) < (p `1 ) - (W-bound C)
by A142, XXREAL_0:2;
then
W-bound (L~ (Cage C,((max (max k1,k2),m') + 1))) > W-bound C
by XREAL_1:15;
hence
contradiction
by Th12;
:: thesis: verum end; A144:
now assume
ii1 >= len (Gauge C,((max (max k1,k2),m') + 1))
;
:: thesis: contradictionthen A145:
ii1 = len (Gauge C,((max (max k1,k2),m') + 1))
by A134, XXREAL_0:1;
((Gauge C,((max (max k1,k2),m') + 1)) * (len (Gauge C,((max (max k1,k2),m') + 1))),jj1) `1 = E-bound (L~ (Cage C,((max (max k1,k2),m') + 1)))
by A96, A134, JORDAN1A:92;
then (Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1 =
E-max (L~ (Cage C,((max (max k1,k2),m') + 1)))
by A99, A103, A105, A145, JORDAN1J:46, SPPOL_2:48
.=
(Upper_Seq C,((max (max k1,k2),m') + 1)) /. (len (Upper_Seq C,((max (max k1,k2),m') + 1)))
by JORDAN1F:7
;
then
i1 = len (Upper_Seq C,((max (max k1,k2),m') + 1))
by A103, A136, PARTFUN2:17;
hence
contradiction
by A100, NAT_1:13;
:: thesis: verum end; A146:
now assume
ii2 <= 1
;
:: thesis: contradictionthen A147:
ii2 = 1
by A135, XXREAL_0:1;
((Gauge C,((max (max k1,k2),m') + 1)) * 1,jj2) `1 = W-bound (L~ (Cage C,((max (max k1,k2),m') + 1)))
by A96, A135, JORDAN1A:94;
then (Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2 =
W-min (L~ (Cage C,((max (max k1,k2),m') + 1)))
by A120, A124, A126, A147, JORDAN1J:47, SPPOL_2:48
.=
(Lower_Seq C,((max (max k1,k2),m') + 1)) /. (len (Lower_Seq C,((max (max k1,k2),m') + 1)))
by JORDAN1F:8
;
then
i2 = len (Lower_Seq C,((max (max k1,k2),m') + 1))
by A124, A136, PARTFUN2:17;
hence
contradiction
by A121, NAT_1:13;
:: thesis: verum end; A148:
now assume
ii2 >= len (Gauge C,((max (max k1,k2),m') + 1))
;
:: thesis: contradictionthen A149:
ii2 = len (Gauge C,((max (max k1,k2),m') + 1))
by A135, XXREAL_0:1;
dist p',
d1 < r
by A131, A137, XXREAL_0:2;
then
dist p',
d1 < min ((p `1 ) - (W-bound C)),
((E-bound C) - (p `1 ))
by A88, XXREAL_0:2;
then A150:
dist p',
d1 < (E-bound C) - (p `1 )
by A139, XXREAL_0:2;
A151:
(((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `1 ) - (p `1 ) <= abs ((((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `1 ) - (p `1 ))
by ABSVALUE:11;
abs ((((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `1 ) - (p `1 )) <= |.(((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) - p).|
by JGRAPH_1:51;
then
abs ((((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `1 ) - (p `1 )) <= |.(p - ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2)).|
by TOPRNS_1:28;
then
(((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `1 ) - (p `1 ) <= |.(p - ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2)).|
by A151, XXREAL_0:2;
then
(E-bound (L~ (Cage C,((max (max k1,k2),m') + 1)))) - (p `1 ) <= |.(p - ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2)).|
by A96, A126, A135, A149, JORDAN1A:92;
then
(E-bound (L~ (Cage C,((max (max k1,k2),m') + 1)))) - (p `1 ) <= dist p',
d1
by SPPOL_1:62;
then
(E-bound (L~ (Cage C,((max (max k1,k2),m') + 1)))) - (p `1 ) < (E-bound C) - (p `1 )
by A150, XXREAL_0:2;
then
E-bound (L~ (Cage C,((max (max k1,k2),m') + 1))) < E-bound C
by XREAL_1:15;
hence
contradiction
by Th10;
:: thesis: verum end; A152:
Ball p',
(rr / 4) c= Ball p',
rr
by A137, PCOMPS_1:1;
A153:
((Gauge C,((max (max k1,k2),m') + 1)) * ii2,jj1) `1 =
((Gauge C,((max (max k1,k2),m') + 1)) * ii2,1) `1
by A134, A135, GOBOARD5:3
.=
((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `1
by A126, A135, GOBOARD5:3
;
A154:
((Gauge C,((max (max k1,k2),m') + 1)) * ii2,jj1) `2 =
((Gauge C,((max (max k1,k2),m') + 1)) * 1,jj1) `2
by A134, A135, GOBOARD5:2
.=
((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `2
by A105, A134, GOBOARD5:2
;
A155:
((Gauge C,((max (max k1,k2),m') + 1)) * ii1,jj2) `1 =
((Gauge C,((max (max k1,k2),m') + 1)) * ii1,1) `1
by A134, A135, GOBOARD5:3
.=
((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `1
by A105, A134, GOBOARD5:3
;
A156:
((Gauge C,((max (max k1,k2),m') + 1)) * ii1,jj2) `2 =
((Gauge C,((max (max k1,k2),m') + 1)) * 1,jj2) `2
by A134, A135, GOBOARD5:2
.=
((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `2
by A126, A135, GOBOARD5:2
;
(
abs ((((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `1 ) - (p `1 )) <= |.(((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) - p).| &
abs ((((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `2 ) - (p `2 )) <= |.(((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) - p).| )
by JGRAPH_1:51;
then
(
abs ((((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `1 ) - (p `1 )) <= |.(p - ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2)).| &
abs ((((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `2 ) - (p `2 )) <= |.(p - ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1)).| )
by TOPRNS_1:28;
then
(
abs ((((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `1 ) - (p `1 )) <= r / 4 &
abs ((((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `2 ) - (p `2 )) <= r / 4 )
by A113, A130, XXREAL_0:2;
then
(abs ((((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `1 ) - (p `1 ))) + (abs ((((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `2 ) - (p `2 ))) <= (r / (2 * 2)) + (r / (2 * 2))
by XREAL_1:9;
then A157:
(abs ((((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `1 ) - (p `1 ))) + (abs ((((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `2 ) - (p `2 ))) < r
by A138, XXREAL_0:2;
(
abs ((((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `1 ) - (p `1 )) <= |.(((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) - p).| &
abs ((((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `2 ) - (p `2 )) <= |.(((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) - p).| )
by JGRAPH_1:51;
then
(
abs ((((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `1 ) - (p `1 )) <= |.(p - ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1)).| &
abs ((((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `2 ) - (p `2 )) <= |.(p - ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2)).| )
by TOPRNS_1:28;
then
(
abs ((((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `1 ) - (p `1 )) <= r / 4 &
abs ((((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `2 ) - (p `2 )) <= r / 4 )
by A113, A130, XXREAL_0:2;
then
(abs ((((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `1 ) - (p `1 ))) + (abs ((((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `2 ) - (p `2 ))) <= (r / (2 * 2)) + (r / (2 * 2))
by XREAL_1:9;
then A158:
(abs ((((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `1 ) - (p `1 ))) + (abs ((((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `2 ) - (p `2 ))) < r
by A138, XXREAL_0:2;
|.(((Gauge C,((max (max k1,k2),m') + 1)) * ii2,jj1) - p).| <= (abs ((((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `1 ) - (p `1 ))) + (abs ((((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `2 ) - (p `2 )))
by A153, A154, JGRAPH_1:49;
then
|.(((Gauge C,((max (max k1,k2),m') + 1)) * ii2,jj1) - p).| < r
by A157, XXREAL_0:2;
then
dist Gij',
p' < r
by SPPOL_1:62;
then A159:
(Gauge C,((max (max k1,k2),m') + 1)) * ii2,
jj1 in Ball p',
r
by METRIC_1:12;
|.(((Gauge C,((max (max k1,k2),m') + 1)) * ii1,jj2) - p).| <= (abs ((((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) `1 ) - (p `1 ))) + (abs ((((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) `2 ) - (p `2 )))
by A155, A156, JGRAPH_1:49;
then
|.(((Gauge C,((max (max k1,k2),m') + 1)) * ii1,jj2) - p).| < r
by A158, XXREAL_0:2;
then
dist Gji',
p' < r
by SPPOL_1:62;
then A160:
(Gauge C,((max (max k1,k2),m') + 1)) * ii1,
jj2 in Ball p',
r
by METRIC_1:12;
A161:
LSeg ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2),
((Gauge C,((max (max k1,k2),m') + 1)) * ii2,jj1) c= Ball p',
rr
by A132, A152, A159, TOPREAL3:28;
A162:
LSeg ((Gauge C,((max (max k1,k2),m') + 1)) * ii2,jj1),
((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) c= Ball p',
rr
by A115, A152, A159, TOPREAL3:28;
A163:
LSeg ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2),
((Gauge C,((max (max k1,k2),m') + 1)) * ii1,jj2) c= Ball p',
rr
by A132, A152, A160, TOPREAL3:28;
A164:
LSeg ((Gauge C,((max (max k1,k2),m') + 1)) * ii1,jj2),
((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) c= Ball p',
rr
by A115, A152, A160, TOPREAL3:28;
now per cases
( jj2 <= jj1 or jj1 < jj2 )
;
suppose A165:
jj2 <= jj1
;
:: thesis: Ball p',r meets Lower_Arc C
(LSeg ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2),((Gauge C,((max (max k1,k2),m') + 1)) * ii2,jj1)) \/ (LSeg ((Gauge C,((max (max k1,k2),m') + 1)) * ii2,jj1),((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1)) c= Ball p',
r
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in (LSeg ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2),((Gauge C,((max (max k1,k2),m') + 1)) * ii2,jj1)) \/ (LSeg ((Gauge C,((max (max k1,k2),m') + 1)) * ii2,jj1),((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1)) or x in Ball p',r )
assume A166:
x in (LSeg ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2),((Gauge C,((max (max k1,k2),m') + 1)) * ii2,jj1)) \/ (LSeg ((Gauge C,((max (max k1,k2),m') + 1)) * ii2,jj1),((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1))
;
:: thesis: x in Ball p',r
then reconsider x' =
x as
Point of
(TOP-REAL 2) ;
now per cases
( x' in LSeg ((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2),((Gauge C,((max (max k1,k2),m') + 1)) * ii2,jj1) or x' in LSeg ((Gauge C,((max (max k1,k2),m') + 1)) * ii2,jj1),((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1) )
by A166, XBOOLE_0:def 3;
end;
hence
x in Ball p',
r
;
:: thesis: verum
end; hence
Ball p',
r meets Lower_Arc C
by A105, A116, A126, A133, A134, A135, A140, A144, A146, A148, A165, JORDAN15:51, XBOOLE_1:63;
:: thesis: verum end; suppose A167:
jj1 < jj2
;
:: thesis: Ball p',r meets Lower_Arc C
(LSeg ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1),((Gauge C,((max (max k1,k2),m') + 1)) * ii1,jj2)) \/ (LSeg ((Gauge C,((max (max k1,k2),m') + 1)) * ii1,jj2),((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2)) c= Ball p',
r
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in (LSeg ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1),((Gauge C,((max (max k1,k2),m') + 1)) * ii1,jj2)) \/ (LSeg ((Gauge C,((max (max k1,k2),m') + 1)) * ii1,jj2),((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2)) or x in Ball p',r )
assume A168:
x in (LSeg ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1),((Gauge C,((max (max k1,k2),m') + 1)) * ii1,jj2)) \/ (LSeg ((Gauge C,((max (max k1,k2),m') + 1)) * ii1,jj2),((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2))
;
:: thesis: x in Ball p',r
then reconsider x' =
x as
Point of
(TOP-REAL 2) ;
now per cases
( x' in LSeg ((Upper_Seq C,((max (max k1,k2),m') + 1)) /. i1),((Gauge C,((max (max k1,k2),m') + 1)) * ii1,jj2) or x' in LSeg ((Gauge C,((max (max k1,k2),m') + 1)) * ii1,jj2),((Lower_Seq C,((max (max k1,k2),m') + 1)) /. i2) )
by A168, XBOOLE_0:def 3;
end;
hence
x in Ball p',
r
;
:: thesis: verum
end; hence
Ball p',
r meets Lower_Arc C
by A105, A116, A126, A133, A134, A135, A140, A144, A146, A148, A167, Th25, XBOOLE_1:63;
:: thesis: verum end; hence
Ball p',
r meets Lower_Arc C
;
:: thesis: verum end;
then
p in Cl (Lower_Arc C)
by A5, GOBOARD6:96;
then
p in Lower_Arc C
by PRE_TOPC:52;
then
p in (Upper_Arc C) /\ (Lower_Arc C)
by A87, 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; :: thesis: verum