let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: union (UBD-Family C) = UBD C
A1: ( UBD (L~ (Cage (C,0))) c= UBD C & UBD (L~ (Cage (C,0))) = LeftComp (Cage (C,0)) ) by Th13, GOBRD14:36;
for X being set st X in UBD-Family C holds
X c= UBD C
proof
let X be set ; :: thesis: ( X in UBD-Family C implies X c= UBD C )
assume X in UBD-Family C ; :: thesis: X c= UBD C
then ex n being Nat st X = UBD (L~ (Cage (C,n))) ;
hence X c= UBD C by Th13; :: thesis: verum
end;
hence union (UBD-Family C) c= UBD C by ZFMISC_1:76; :: according to XBOOLE_0:def 10 :: thesis: UBD C c= union (UBD-Family C)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in UBD C or x in union (UBD-Family C) )
assume A2: x in UBD C ; :: thesis: x in union (UBD-Family C)
UBD C = union { B where B is Subset of (TOP-REAL 2) : B is_outside_component_of C } by JORDAN2C:def 5;
then consider A being set such that
A3: x in A and
A4: A in { B where B is Subset of (TOP-REAL 2) : B is_outside_component_of C } by A2, TARSKI:def 4;
ex B being Subset of (TOP-REAL 2) st
( A = B & B is_outside_component_of C ) by A4;
then reconsider p = x as Point of (TOP-REAL 2) by A3;
consider q being Point of (TOP-REAL 2) such that
A5: q `2 > N-bound (L~ (Cage (C,0))) and
A6: p <> q by TOPREAL6:33;
(Cage (C,0)) /. 1 = N-min (L~ (Cage (C,0))) by JORDAN9:32;
then q in LeftComp (Cage (C,0)) by A5, JORDAN2C:113;
then consider P being Subset of (TOP-REAL 2) such that
A7: P is_S-P_arc_joining p,q and
A8: P c= UBD C by A2, A6, A1, TOPREAL4:29;
consider f being FinSequence of (TOP-REAL 2) such that
A9: f is being_S-Seq and
A10: P = L~ f and
A11: p = f /. 1 and
q = f /. (len f) by A7, TOPREAL4:def 1;
reconsider f = f as being_S-Seq FinSequence of (TOP-REAL 2) by A9;
2 <= len f by NAT_D:60;
then A12: x in P by A10, A11, JORDAN3:1;
( not L~ f is empty & TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) ) by EUCLID:def 8;
then reconsider P1 = P, C1 = C as non empty compact Subset of (TopSpaceMetr (Euclid 2)) by A10, COMPTS_1:23;
set d = min_dist_min (P1,C1);
UBD C is_outside_component_of C by JORDAN2C:68;
then UBD C is_a_component_of C ` by JORDAN2C:def 3;
then C misses UBD C by JORDAN2C:117;
then P misses C by A8, XBOOLE_1:63;
then min_dist_min (P1,C1) > 0 by JGRAPH_1:38;
then (min_dist_min (P1,C1)) / 2 > 0 by XREAL_1:139;
then consider n being Nat such that
1 < n and
A13: ( dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < (min_dist_min (P1,C1)) / 2 & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < (min_dist_min (P1,C1)) / 2 ) by GOBRD14:11;
set G = Gauge (C,n);
set g = Cage (C,n);
A14: UBD (L~ (Cage (C,n))) in UBD-Family C ;
A15: now :: thesis: not (L~ (Cage (C,n))) /\ P <> {}
assume (L~ (Cage (C,n))) /\ P <> {} ; :: thesis: contradiction
then consider a being object such that
A16: a in (L~ (Cage (C,n))) /\ P by XBOOLE_0:def 1;
a in L~ (Cage (C,n)) by A16, XBOOLE_0:def 4;
then consider i being Nat such that
A17: ( 1 <= i & i + 1 <= len (Cage (C,n)) ) and
A18: a in LSeg ((Cage (C,n)),i) by SPPOL_2:13;
right_cell ((Cage (C,n)),i,(Gauge (C,n))) meets C by A17, JORDAN9:31;
then consider c being object such that
A19: c in (right_cell ((Cage (C,n)),i,(Gauge (C,n)))) /\ C by XBOOLE_0:4;
reconsider c = c as Point of (Euclid 2) by A19, TOPREAL3:8;
reconsider a9 = a as Point of (Euclid 2) by A16, TOPREAL3:8;
A20: c in C by A19, XBOOLE_0:def 4;
reconsider c9 = c as Point of (TOP-REAL 2) by A19;
A21: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def 1;
then consider i1, j1, i2, j2 being Nat such that
A22: [i1,j1] in Indices (Gauge (C,n)) and
A23: (Cage (C,n)) /. i = (Gauge (C,n)) * (i1,j1) and
A24: [i2,j2] in Indices (Gauge (C,n)) and
A25: (Cage (C,n)) /. (i + 1) = (Gauge (C,n)) * (i2,j2) and
A26: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A17, JORDAN8:3;
(left_cell ((Cage (C,n)),i,(Gauge (C,n)))) /\ (right_cell ((Cage (C,n)),i,(Gauge (C,n)))) = LSeg ((Cage (C,n)),i) by A17, A21, GOBRD13:29;
then A27: a in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by A18, XBOOLE_0:def 4;
a in P by A16, XBOOLE_0:def 4;
then A28: dist (a9,c) >= min_dist_min (P1,C1) by A20, WEIERSTR:34;
reconsider A = a as Point of (TOP-REAL 2) by A16;
set e = E-bound C;
set w = W-bound C;
set p = N-bound C;
set s = S-bound C;
A29: 4 <= len (Gauge (C,n)) by JORDAN8:10;
then A30: 1 <= len (Gauge (C,n)) by XXREAL_0:2;
A31: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;
then A32: 1 <= width (Gauge (C,n)) by A29, XXREAL_0:2;
A33: [1,1] in Indices (Gauge (C,n)) by A31, A30, MATRIX_0:30;
A34: c in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by A19, XBOOLE_0:def 4;
now :: thesis: ( ( i1 = i2 & j1 + 1 = j2 & dist (A,c9) <= (((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n)) ) or ( i1 + 1 = i2 & j1 = j2 & dist (A,c9) <= (((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n)) ) or ( i1 = i2 + 1 & j1 = j2 & dist (A,c9) <= (((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n)) ) or ( i1 = i2 & j1 = j2 + 1 & dist (A,c9) <= (((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n)) ) )
per cases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A26;
case A35: ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis: dist (A,c9) <= (((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n))
then A36: i1 < len (Gauge (C,n)) by A17, A22, A23, A24, A25, Th1;
then A37: i1 + 1 <= len (Gauge (C,n)) by NAT_1:13;
A38: 1 <= i1 by A22, MATRIX_0:32;
then 1 <= i1 + 1 by NAT_1:13;
then A39: [(i1 + 1),1] in Indices (Gauge (C,n)) by A32, A37, MATRIX_0:30;
[i1,1] in Indices (Gauge (C,n)) by A32, A38, A36, MATRIX_0:30;
then A40: ( dist (((Gauge (C,n)) * (i1,1)),((Gauge (C,n)) * ((i1 + 1),1))) = (((Gauge (C,n)) * ((i1 + 1),1)) `1) - (((Gauge (C,n)) * (i1,1)) `1) & dist (((Gauge (C,n)) * (i1,1)),((Gauge (C,n)) * ((i1 + 1),1))) = ((E-bound C) - (W-bound C)) / (2 |^ n) ) by A39, GOBRD14:5, GOBRD14:10;
A41: j1 + 1 <= width (Gauge (C,n)) by A24, A35, MATRIX_0:32;
then A42: j1 < width (Gauge (C,n)) by NAT_1:13;
A43: 1 <= j1 by A22, MATRIX_0:32;
then 1 <= j1 + 1 by NAT_1:13;
then A44: [1,(j1 + 1)] in Indices (Gauge (C,n)) by A30, A41, MATRIX_0:30;
A45: right_cell ((Cage (C,n)),i,(Gauge (C,n))) = cell ((Gauge (C,n)),i1,j1) by A17, A21, A22, A23, A24, A25, A35, GOBRD13:22
.= { |[r,t]| where r, t is Real : ( ((Gauge (C,n)) * (i1,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i1 + 1),1)) `1 & ((Gauge (C,n)) * (1,j1)) `2 <= t & t <= ((Gauge (C,n)) * (1,(j1 + 1))) `2 ) } by A38, A36, A43, A42, GOBRD11:32 ;
then consider aa, ab being Real such that
A46: a = |[aa,ab]| and
A47: ( ((Gauge (C,n)) * (i1,1)) `1 <= aa & aa <= ((Gauge (C,n)) * ((i1 + 1),1)) `1 & ((Gauge (C,n)) * (1,j1)) `2 <= ab & ab <= ((Gauge (C,n)) * (1,(j1 + 1))) `2 ) by A27;
A48: ( A `1 = aa & A `2 = ab ) by A46, EUCLID:52;
[1,j1] in Indices (Gauge (C,n)) by A30, A43, A42, MATRIX_0:30;
then A49: ( dist (((Gauge (C,n)) * (1,j1)),((Gauge (C,n)) * (1,(j1 + 1)))) = (((Gauge (C,n)) * (1,(j1 + 1))) `2) - (((Gauge (C,n)) * (1,j1)) `2) & dist (((Gauge (C,n)) * (1,j1)),((Gauge (C,n)) * (1,(j1 + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ n) ) by A44, GOBRD14:6, GOBRD14:9;
consider r, t being Real such that
A50: c = |[r,t]| and
A51: ( ((Gauge (C,n)) * (i1,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i1 + 1),1)) `1 & ((Gauge (C,n)) * (1,j1)) `2 <= t & t <= ((Gauge (C,n)) * (1,(j1 + 1))) `2 ) by A34, A45;
( c9 `1 = r & c9 `2 = t ) by A50, EUCLID:52;
hence dist (A,c9) <= (((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n)) by A51, A47, A48, A49, A40, TOPREAL6:95; :: thesis: verum
end;
case A52: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis: dist (A,c9) <= (((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n))
then A53: i1 + 1 <= len (Gauge (C,n)) by A24, MATRIX_0:32;
then A54: i1 < len (Gauge (C,n)) by NAT_1:13;
A55: 1 <= i1 by A22, MATRIX_0:32;
then 1 <= i1 + 1 by NAT_1:13;
then A56: [(i1 + 1),1] in Indices (Gauge (C,n)) by A32, A53, MATRIX_0:30;
[i1,1] in Indices (Gauge (C,n)) by A32, A55, A54, MATRIX_0:30;
then A57: ( dist (((Gauge (C,n)) * (i1,1)),((Gauge (C,n)) * ((i1 + 1),1))) = (((Gauge (C,n)) * ((i1 + 1),1)) `1) - (((Gauge (C,n)) * (i1,1)) `1) & dist (((Gauge (C,n)) * (i1,1)),((Gauge (C,n)) * ((i1 + 1),1))) = ((E-bound C) - (W-bound C)) / (2 |^ n) ) by A56, GOBRD14:5, GOBRD14:10;
A58: j2 <= width (Gauge (C,n)) by A24, MATRIX_0:32;
j2 > 1 by A17, A22, A23, A24, A25, A52, Th3;
then A59: j2 - 1 > 0 by XREAL_1:50;
then A60: j2 - 1 = j2 -' 1 by XREAL_0:def 2;
then A61: 1 <= j2 -' 1 by A59, NAT_1:14;
(width (Gauge (C,n))) - 1 < (width (Gauge (C,n))) - 0 by XREAL_1:15;
then A62: j2 -' 1 < width (Gauge (C,n)) by A60, A58, XREAL_1:15;
then A63: [1,(j2 -' 1)] in Indices (Gauge (C,n)) by A30, A61, MATRIX_0:30;
A64: right_cell ((Cage (C,n)),i,(Gauge (C,n))) = cell ((Gauge (C,n)),i1,(j2 -' 1)) by A17, A21, A22, A23, A24, A25, A52, GOBRD13:24
.= { |[r,t]| where r, t is Real : ( ((Gauge (C,n)) * (i1,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i1 + 1),1)) `1 & ((Gauge (C,n)) * (1,(j2 -' 1))) `2 <= t & t <= ((Gauge (C,n)) * (1,((j2 -' 1) + 1))) `2 ) } by A55, A54, A61, A62, GOBRD11:32 ;
then consider aa, ab being Real such that
A65: a = |[aa,ab]| and
A66: ( ((Gauge (C,n)) * (i1,1)) `1 <= aa & aa <= ((Gauge (C,n)) * ((i1 + 1),1)) `1 & ((Gauge (C,n)) * (1,(j2 -' 1))) `2 <= ab & ab <= ((Gauge (C,n)) * (1,((j2 -' 1) + 1))) `2 ) by A27;
A67: ( A `1 = aa & A `2 = ab ) by A65, EUCLID:52;
1 <= (j2 -' 1) + 1 by A61, NAT_1:13;
then [1,((j2 -' 1) + 1)] in Indices (Gauge (C,n)) by A30, A60, A58, MATRIX_0:30;
then A68: ( dist (((Gauge (C,n)) * (1,(j2 -' 1))),((Gauge (C,n)) * (1,((j2 -' 1) + 1)))) = (((Gauge (C,n)) * (1,((j2 -' 1) + 1))) `2) - (((Gauge (C,n)) * (1,(j2 -' 1))) `2) & dist (((Gauge (C,n)) * (1,(j2 -' 1))),((Gauge (C,n)) * (1,((j2 -' 1) + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ n) ) by A63, GOBRD14:6, GOBRD14:9;
consider r, t being Real such that
A69: c = |[r,t]| and
A70: ( ((Gauge (C,n)) * (i1,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i1 + 1),1)) `1 & ((Gauge (C,n)) * (1,(j2 -' 1))) `2 <= t & t <= ((Gauge (C,n)) * (1,((j2 -' 1) + 1))) `2 ) by A34, A64;
( c9 `1 = r & c9 `2 = t ) by A69, EUCLID:52;
hence dist (A,c9) <= (((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n)) by A70, A66, A67, A68, A57, TOPREAL6:95; :: thesis: verum
end;
case A71: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis: dist (A,c9) <= (((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n))
A72: 1 <= j1 + 1 by NAT_1:12;
A73: j1 < width (Gauge (C,n)) by A17, A22, A23, A24, A25, A71, Th4;
then j1 + 1 <= width (Gauge (C,n)) by NAT_1:13;
then A74: [1,(j1 + 1)] in Indices (Gauge (C,n)) by A30, A72, MATRIX_0:30;
A75: 1 <= j1 by A22, MATRIX_0:32;
then [1,j1] in Indices (Gauge (C,n)) by A30, A73, MATRIX_0:30;
then A76: ( dist (((Gauge (C,n)) * (1,j1)),((Gauge (C,n)) * (1,(j1 + 1)))) = (((Gauge (C,n)) * (1,(j1 + 1))) `2) - (((Gauge (C,n)) * (1,j1)) `2) & dist (((Gauge (C,n)) * (1,j1)),((Gauge (C,n)) * (1,(j1 + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ n) ) by A74, GOBRD14:6, GOBRD14:9;
A77: i2 + 1 <= len (Gauge (C,n)) by A22, A71, MATRIX_0:32;
then A78: i2 < len (Gauge (C,n)) by NAT_1:13;
A79: 1 <= i2 by A24, MATRIX_0:32;
then 1 <= i2 + 1 by NAT_1:13;
then A80: [(i2 + 1),1] in Indices (Gauge (C,n)) by A32, A77, MATRIX_0:30;
A81: right_cell ((Cage (C,n)),i,(Gauge (C,n))) = cell ((Gauge (C,n)),i2,j1) by A17, A21, A22, A23, A24, A25, A71, GOBRD13:26
.= { |[r,t]| where r, t is Real : ( ((Gauge (C,n)) * (i2,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i2 + 1),1)) `1 & ((Gauge (C,n)) * (1,j1)) `2 <= t & t <= ((Gauge (C,n)) * (1,(j1 + 1))) `2 ) } by A79, A78, A75, A73, GOBRD11:32 ;
then consider aa, ab being Real such that
A82: a = |[aa,ab]| and
A83: ( ((Gauge (C,n)) * (i2,1)) `1 <= aa & aa <= ((Gauge (C,n)) * ((i2 + 1),1)) `1 & ((Gauge (C,n)) * (1,j1)) `2 <= ab & ab <= ((Gauge (C,n)) * (1,(j1 + 1))) `2 ) by A27;
A84: ( A `1 = aa & A `2 = ab ) by A82, EUCLID:52;
[i2,1] in Indices (Gauge (C,n)) by A32, A79, A78, MATRIX_0:30;
then A85: ( dist (((Gauge (C,n)) * (i2,1)),((Gauge (C,n)) * ((i2 + 1),1))) = (((Gauge (C,n)) * ((i2 + 1),1)) `1) - (((Gauge (C,n)) * (i2,1)) `1) & dist (((Gauge (C,n)) * (i2,1)),((Gauge (C,n)) * ((i2 + 1),1))) = ((E-bound C) - (W-bound C)) / (2 |^ n) ) by A80, GOBRD14:5, GOBRD14:10;
consider r, t being Real such that
A86: c = |[r,t]| and
A87: ( ((Gauge (C,n)) * (i2,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i2 + 1),1)) `1 & ((Gauge (C,n)) * (1,j1)) `2 <= t & t <= ((Gauge (C,n)) * (1,(j1 + 1))) `2 ) by A34, A81;
( c9 `1 = r & c9 `2 = t ) by A86, EUCLID:52;
hence dist (A,c9) <= (((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n)) by A87, A83, A84, A76, A85, TOPREAL6:95; :: thesis: verum
end;
case A88: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis: dist (A,c9) <= (((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n))
then A89: j2 + 1 <= width (Gauge (C,n)) by A22, MATRIX_0:32;
then A90: j2 < width (Gauge (C,n)) by NAT_1:13;
A91: 1 <= j2 by A24, MATRIX_0:32;
then 1 <= j2 + 1 by NAT_1:13;
then A92: [1,(j2 + 1)] in Indices (Gauge (C,n)) by A30, A89, MATRIX_0:30;
[1,j2] in Indices (Gauge (C,n)) by A30, A91, A90, MATRIX_0:30;
then A93: ( dist (((Gauge (C,n)) * (1,j2)),((Gauge (C,n)) * (1,(j2 + 1)))) = (((Gauge (C,n)) * (1,(j2 + 1))) `2) - (((Gauge (C,n)) * (1,j2)) `2) & dist (((Gauge (C,n)) * (1,j2)),((Gauge (C,n)) * (1,(j2 + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ n) ) by A92, GOBRD14:6, GOBRD14:9;
A94: i1 <= len (Gauge (C,n)) by A22, MATRIX_0:32;
i1 > 1 by A17, A22, A23, A24, A25, A88, Th2;
then A95: i1 - 1 > 0 by XREAL_1:50;
then A96: i1 - 1 = i1 -' 1 by XREAL_0:def 2;
then A97: 1 <= i1 -' 1 by A95, NAT_1:14;
(len (Gauge (C,n))) - 1 < (len (Gauge (C,n))) - 0 by XREAL_1:15;
then A98: i1 -' 1 < len (Gauge (C,n)) by A96, A94, XREAL_1:15;
then A99: [(i1 -' 1),1] in Indices (Gauge (C,n)) by A32, A97, MATRIX_0:30;
A100: right_cell ((Cage (C,n)),i,(Gauge (C,n))) = cell ((Gauge (C,n)),(i1 -' 1),j2) by A17, A21, A22, A23, A24, A25, A88, GOBRD13:28
.= { |[r,t]| where r, t is Real : ( ((Gauge (C,n)) * ((i1 -' 1),1)) `1 <= r & r <= ((Gauge (C,n)) * (((i1 -' 1) + 1),1)) `1 & ((Gauge (C,n)) * (1,j2)) `2 <= t & t <= ((Gauge (C,n)) * (1,(j2 + 1))) `2 ) } by A97, A98, A91, A90, GOBRD11:32 ;
then consider aa, ab being Real such that
A101: a = |[aa,ab]| and
A102: ( ((Gauge (C,n)) * ((i1 -' 1),1)) `1 <= aa & aa <= ((Gauge (C,n)) * (((i1 -' 1) + 1),1)) `1 & ((Gauge (C,n)) * (1,j2)) `2 <= ab & ab <= ((Gauge (C,n)) * (1,(j2 + 1))) `2 ) by A27;
A103: ( A `1 = aa & A `2 = ab ) by A101, EUCLID:52;
1 <= (i1 -' 1) + 1 by A97, NAT_1:13;
then [((i1 -' 1) + 1),1] in Indices (Gauge (C,n)) by A32, A96, A94, MATRIX_0:30;
then A104: ( dist (((Gauge (C,n)) * ((i1 -' 1),1)),((Gauge (C,n)) * (((i1 -' 1) + 1),1))) = (((Gauge (C,n)) * (((i1 -' 1) + 1),1)) `1) - (((Gauge (C,n)) * ((i1 -' 1),1)) `1) & dist (((Gauge (C,n)) * ((i1 -' 1),1)),((Gauge (C,n)) * (((i1 -' 1) + 1),1))) = ((E-bound C) - (W-bound C)) / (2 |^ n) ) by A99, GOBRD14:5, GOBRD14:10;
consider r, t being Real such that
A105: c = |[r,t]| and
A106: ( ((Gauge (C,n)) * ((i1 -' 1),1)) `1 <= r & r <= ((Gauge (C,n)) * (((i1 -' 1) + 1),1)) `1 & ((Gauge (C,n)) * (1,j2)) `2 <= t & t <= ((Gauge (C,n)) * (1,(j2 + 1))) `2 ) by A34, A100;
( c9 `1 = r & c9 `2 = t ) by A105, EUCLID:52;
hence dist (A,c9) <= (((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n)) by A106, A102, A103, A93, A104, TOPREAL6:95; :: thesis: verum
end;
end;
end;
then A107: dist (a9,c) <= (((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n)) by TOPREAL6:def 1;
1 + 1 <= len (Gauge (C,n)) by A29, XXREAL_0:2;
then [(1 + 1),1] in Indices (Gauge (C,n)) by A32, MATRIX_0:30;
then A108: dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * ((1 + 1),1))) = ((E-bound C) - (W-bound C)) / (2 |^ n) by A33, GOBRD14:10;
1 + 1 <= width (Gauge (C,n)) by A31, A29, XXREAL_0:2;
then [1,(1 + 1)] in Indices (Gauge (C,n)) by A30, MATRIX_0:30;
then dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,(1 + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ n) by A33, GOBRD14:9;
then (((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n)) < ((min_dist_min (P1,C1)) / 2) + ((min_dist_min (P1,C1)) / 2) by A13, A108, XREAL_1:8;
hence contradiction by A28, A107, XXREAL_0:2; :: thesis: verum
end;
A109: P c= (L~ (Cage (C,n))) `
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in P or a in (L~ (Cage (C,n))) ` )
assume A110: a in P ; :: thesis: a in (L~ (Cage (C,n))) `
then not a in L~ (Cage (C,n)) by A15, XBOOLE_0:def 4;
hence a in (L~ (Cage (C,n))) ` by A110, SUBSET_1:29; :: thesis: verum
end;
( 0 < n or 0 = n ) ;
then N-bound (L~ (Cage (C,0))) >= N-bound (L~ (Cage (C,n))) by Th7;
then ( (Cage (C,n)) /. 1 = N-min (L~ (Cage (C,n))) & q `2 > N-bound (L~ (Cage (C,n))) ) by A5, JORDAN9:32, XXREAL_0:2;
then q in LeftComp (Cage (C,n)) by JORDAN2C:113;
then q in UBD (L~ (Cage (C,n))) by GOBRD14:36;
then A111: {q} c= UBD (L~ (Cage (C,n))) by ZFMISC_1:31;
A112: P is_an_arc_of p,q by A7, TOPREAL4:2;
now :: thesis: ex a being Point of (TOP-REAL 2) st
( a in {q} & a in P )
take a = q; :: thesis: ( a in {q} & a in P )
thus ( a in {q} & a in P ) by A112, TARSKI:def 1, TOPREAL1:1; :: thesis: verum
end;
then A113: {q} meets P by XBOOLE_0:3;
UBD (L~ (Cage (C,n))) is_outside_component_of L~ (Cage (C,n)) by JORDAN2C:68;
then ex E being Subset of ((TOP-REAL 2) | ((L~ (Cage (C,n))) `)) st
( E = UBD (L~ (Cage (C,n))) & E is a_component & E is not bounded Subset of (Euclid 2) ) by JORDAN2C:14;
then UBD (L~ (Cage (C,n))) is_a_component_of (L~ (Cage (C,n))) ` by CONNSP_1:def 6;
then P c= UBD (L~ (Cage (C,n))) by A109, A112, A111, A113, GOBOARD9:4, JORDAN6:10;
hence x in union (UBD-Family C) by A12, A14, TARSKI:def 4; :: thesis: verum