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:46;
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 Element of 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:94; :: according to XBOOLE_0:def 10 :: thesis: UBD C c= union (UBD-Family C)
let x be set ; :: 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 6;
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:41;
(Cage C,0 ) /. 1 = N-min (L~ (Cage C,0 )) by JORDAN9:34;
then q in LeftComp (Cage C,0 ) by A5, JORDAN2C:121;
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:30;
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 REALSET1:13;
then A12: x in P by A10, A11, JORDAN3:34;
( 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:33;
set d = min_dist_min P1,C1;
UBD C is_outside_component_of C by JORDAN2C:76;
then UBD C is_a_component_of C ` by JORDAN2C:def 4;
then C misses UBD C by JORDAN2C:125;
then P misses C by A8, XBOOLE_1:63;
then min_dist_min P1,C1 > 0 by JGRAPH_1:55;
then (min_dist_min P1,C1) / 2 > 0 by XREAL_1:141;
then consider n being Element of 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:21;
set G = Gauge C,n;
set g = Cage C,n;
A14: UBD (L~ (Cage C,n)) in UBD-Family C ;

A15: now

assume (L~ (Cage C,n)) /\ P <> {} ; :: thesis: contradiction
then consider a being set 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 Element of 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:33;
then consider c being set 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:13;
reconsider a9 = a as Point of (Euclid 2) by A16, TOPREAL3:13;
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 Element of 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:6;
(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:30;
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:40;
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:13;
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_1:37;
A34: c in right_cell (Cage C,n),i,(Gauge C,n) by A19, XBOOLE_0:def 4;

now

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_1:39;
then 1 <= i1 + 1 by NAT_1:13;
then A39: [(i1 + 1),1] in Indices (Gauge C,n) by A32, A37, MATRIX_1:37;
[i1,1] in Indices (Gauge C,n) by A32, A38, A36, MATRIX_1:37;
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:15, GOBRD14:20;
A41: j1 + 1 <= width (Gauge C,n) by A24, A35, MATRIX_1:39;
then A42: j1 < width (Gauge C,n) by NAT_1:13;
A43: 1 <= j1 by A22, MATRIX_1:39;
then 1 <= j1 + 1 by NAT_1:13;
then A44: [1,(j1 + 1)] in Indices (Gauge C,n) by A30, A41, MATRIX_1:37;
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:23
.= { |[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:56;
[1,j1] in Indices (Gauge C,n) by A30, A43, A42, MATRIX_1:37;
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:16, GOBRD14:19;
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:56;
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:104; :: 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_1:39;
then A54: i1 < len (Gauge C,n) by NAT_1:13;
A55: 1 <= i1 by A22, MATRIX_1:39;
then 1 <= i1 + 1 by NAT_1:13;
then A56: [(i1 + 1),1] in Indices (Gauge C,n) by A32, A53, MATRIX_1:37;
[i1,1] in Indices (Gauge C,n) by A32, A55, A54, MATRIX_1:37;
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:15, GOBRD14:20;
A58: j2 <= width (Gauge C,n) by A24, MATRIX_1:39;
j2 > 1 by A17, A22, A23, A24, A25, A52, Th3;
then A59: j2 - 1 > 0 by XREAL_1:52;
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:17;
then A62: j2 -' 1 < width (Gauge C,n) by A60, A58, XREAL_1:17;
then A63: [1,(j2 -' 1)] in Indices (Gauge C,n) by A30, A61, MATRIX_1:37;
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:25
.= { |[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:56;
1 <= (j2 -' 1) + 1 by A61, NAT_1:13;
then [1,((j2 -' 1) + 1)] in Indices (Gauge C,n) by A30, A60, A58, MATRIX_1:37;
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:16, GOBRD14:19;
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:56;
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:104; :: 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_1:37;
A75: 1 <= j1 by A22, MATRIX_1:39;
then [1,j1] in Indices (Gauge C,n) by A30, A73, MATRIX_1:37;
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:16, GOBRD14:19;
A77: i2 + 1 <= len (Gauge C,n) by A22, A71, MATRIX_1:39;
then A78: i2 < len (Gauge C,n) by NAT_1:13;
A79: 1 <= i2 by A24, MATRIX_1:39;
then 1 <= i2 + 1 by NAT_1:13;
then A80: [(i2 + 1),1] in Indices (Gauge C,n) by A32, A77, MATRIX_1:37;
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:27
.= { |[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:56;
[i2,1] in Indices (Gauge C,n) by A32, A79, A78, MATRIX_1:37;
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:15, GOBRD14:20;
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:56;
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:104; :: 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_1:39;
then A90: j2 < width (Gauge C,n) by NAT_1:13;
A91: 1 <= j2 by A24, MATRIX_1:39;
then 1 <= j2 + 1 by NAT_1:13;
then A92: [1,(j2 + 1)] in Indices (Gauge C,n) by A30, A89, MATRIX_1:37;
[1,j2] in Indices (Gauge C,n) by A30, A91, A90, MATRIX_1:37;
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:16, GOBRD14:19;
A94: i1 <= len (Gauge C,n) by A22, MATRIX_1:39;
i1 > 1 by A17, A22, A23, A24, A25, A88, Th2;
then A95: i1 - 1 > 0 by XREAL_1:52;
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:17;
then A98: i1 -' 1 < len (Gauge C,n) by A96, A94, XREAL_1:17;
then A99: [(i1 -' 1),1] in Indices (Gauge C,n) by A32, A97, MATRIX_1:37;
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:29
.= { |[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:56;
1 <= (i1 -' 1) + 1 by A97, NAT_1:13;
then [((i1 -' 1) + 1),1] in Indices (Gauge C,n) by A32, A96, A94, MATRIX_1:37;
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:15, GOBRD14:20;
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:56;
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:104; :: 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_1:37;
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:20;
1 + 1 <= width (Gauge C,n) by A31, A29, XXREAL_0:2;
then [1,(1 + 1)] in Indices (Gauge C,n) by A30, MATRIX_1:37;
then dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,(1 + 1)) = ((N-bound C) - (S-bound C)) / (2 |^ n) by A33, GOBRD14:19;
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:10;
hence contradiction by A28, A107, XXREAL_0:2; :: thesis: verum

end;

A109: P c= (L~ (Cage C,n)) `

proof

let a be set ; :: 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:50; :: thesis: verum

end;

( 0 < n or 0 = n ) by NAT_1:2;
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:34, XXREAL_0:2;
then q in LeftComp (Cage C,n) by JORDAN2C:121;
then q in UBD (L~ (Cage C,n)) by GOBRD14:46;
then A111: {q} c= UBD (L~ (Cage C,n)) by ZFMISC_1:37;
A112: P is_an_arc_of p,q by A7, TOPREAL4:3;

now

take a = q; :: thesis: ( a in {q} & a in P )
thus ( a in {q} & a in P ) by A112, TARSKI:def 1, TOPREAL1:4; :: 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:76;
then ex E being Subset of ((TOP-REAL 2) | ((L~ (Cage C,n)) ` )) st
( E = UBD (L~ (Cage C,n)) & E is_a_component_of (TOP-REAL 2) | ((L~ (Cage C,n)) ` ) & E is not bounded Subset of (Euclid 2) ) by JORDAN2C:18;
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:6, JORDAN6:11;
hence x in union (UBD-Family C) by A12, A14, TARSKI:def 4; :: thesis: verum