let C be Simple_closed_curve; :: thesis: UMP C in North_Arc C
set w = ((W-bound C) + (E-bound C)) / 2;
set p = UMP C;
set U = { (UMP (Upper_Arc (L~ (Cage C,n)))) where n is Element of NAT : 0 < n } ;
{ (UMP (Upper_Arc (L~ (Cage C,n)))) where n is Element of NAT : 0 < n } c= the carrier of (TOP-REAL 2)
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (UMP (Upper_Arc (L~ (Cage C,n)))) where n is Element of NAT : 0 < n } or x in the carrier of (TOP-REAL 2) )
assume x in { (UMP (Upper_Arc (L~ (Cage C,n)))) where n is Element of NAT : 0 < n } ; :: thesis: x in the carrier of (TOP-REAL 2)
then ex n being Element of NAT st
( x = UMP (Upper_Arc (L~ (Cage C,n))) & 0 < n ) ;
hence x in the carrier of (TOP-REAL 2) ; :: thesis: verum
end;
then reconsider U = { (UMP (Upper_Arc (L~ (Cage C,n)))) where n is Element of NAT : 0 < n } as Subset of (TOP-REAL 2) ;
set n0 = N-bound (L~ (Cage C,1));
set H = LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|;
set q = lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U));
set S = LSeg |[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|;
A1: |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:56;
A2: |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 = N-bound C by EUCLID:56;
A3: |[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]| `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:56;
A4: |[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]| `2 = N-bound (L~ (Cage C,1)) by EUCLID:56;
A5: |[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)))]| `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:56;
A6: |[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)))]| `2 = lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)) by EUCLID:56;
A7: |[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)))]| in LSeg |[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]| by RLTOPSP1:69;
A8: (UMP C) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:56;
A9: LSeg |[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]| is vertical by A3, A5, SPPOL_1:37;
A10: (LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|) /\ C = {(UMP C)} by JORDAN21:47;
A11: for n being Element of NAT holds (UMP (Upper_Arc (L~ (Cage C,n)))) `1 = ((W-bound C) + (E-bound C)) / 2
proof
let n be Element of NAT ; :: thesis: (UMP (Upper_Arc (L~ (Cage C,n)))) `1 = ((W-bound C) + (E-bound C)) / 2
A12: (W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n))) = (W-bound C) + (E-bound C) by JORDAN1G:41;
thus (UMP (Upper_Arc (L~ (Cage C,n)))) `1 = ((W-bound (Upper_Arc (L~ (Cage C,n)))) + (E-bound (Upper_Arc (L~ (Cage C,n))))) / 2 by EUCLID:56
.= ((W-bound (L~ (Cage C,n))) + (E-bound (Upper_Arc (L~ (Cage C,n))))) / 2 by JORDAN21:26
.= ((W-bound C) + (E-bound C)) / 2 by A12, JORDAN21:27 ; :: thesis: verum
end;
A13: for n being Element of NAT st 0 < n holds
(UMP (Upper_Arc (L~ (Cage C,n)))) `2 in proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)
proof
let n be Element of NAT ; :: thesis: ( 0 < n implies (UMP (Upper_Arc (L~ (Cage C,n)))) `2 in proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U) )
set f = Cage C,n;
set s = UMP (Upper_Arc (L~ (Cage C,n)));
A14: (UMP (Upper_Arc (L~ (Cage C,n)))) `2 <= N-bound (L~ (Cage C,n)) by JORDAN21:60;
assume A15: 0 < n ; :: thesis: (UMP (Upper_Arc (L~ (Cage C,n)))) `2 in proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)
then 0 + 1 <= n by NAT_1:13;
then ( 1 < n or n = 1 ) by XXREAL_0:1;
then N-bound (L~ (Cage C,n)) <= N-bound (L~ (Cage C,1)) by JORDAN10:7;
then A16: (UMP (Upper_Arc (L~ (Cage C,n)))) `2 <= N-bound (L~ (Cage C,1)) by A14, XXREAL_0:2;
A17: (UMP (Upper_Arc (L~ (Cage C,n)))) `1 = ((W-bound C) + (E-bound C)) / 2 by A11;
(UMP C) `2 <= (UMP (Upper_Arc (L~ (Cage C,n)))) `2 by A15, Th25;
then A18: UMP (Upper_Arc (L~ (Cage C,n))) in LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]| by A3, A4, A8, A16, A17, GOBOARD7:8;
UMP (Upper_Arc (L~ (Cage C,n))) in U by A15;
then A19: UMP (Upper_Arc (L~ (Cage C,n))) in (LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U by A18, XBOOLE_0:def 4;
(UMP (Upper_Arc (L~ (Cage C,n)))) `2 = proj2 . (UMP (Upper_Arc (L~ (Cage C,n)))) by PSCOMP_1:def 29;
hence (UMP (Upper_Arc (L~ (Cage C,n)))) `2 in proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U) by A19, FUNCT_2:43; :: thesis: verum
end;
(LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U is Bounded by TOPREAL6:98;
then proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U) is bounded by JCT_MISC:23;
then A20: proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U) is bounded_below by XXREAL_2:def 11;
A21: (UMP (Upper_Arc (L~ (Cage C,1)))) `2 <= N-bound (L~ (Cage C,1)) by JORDAN21:60;
A22: (UMP C) `2 <= (UMP (Upper_Arc (L~ (Cage C,1)))) `2 by Th25;
A23: (UMP (Upper_Arc (L~ (Cage C,1)))) `2 in proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U) by A13;
then lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)) <= (UMP (Upper_Arc (L~ (Cage C,1)))) `2 by A20, SEQ_4:def 5;
then A24: lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)) <= N-bound (L~ (Cage C,1)) by A21, XXREAL_0:2;
per cases ( UMP C <> |[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)))]| or UMP C = |[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)))]| ) ;
suppose A25: UMP C <> |[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)))]| ; :: thesis: UMP C in North_Arc C
A26: now
assume A27: (UMP C) `2 >= lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)) ; :: thesis: contradiction
per cases ( (UMP C) `2 = lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)) or (UMP C) `2 > lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)) ) by A27, XXREAL_0:1;
suppose (UMP C) `2 = lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)) ; :: thesis: contradiction
hence contradiction by A25, EUCLID:56; :: thesis: verum
end;
suppose (UMP C) `2 > lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)) ; :: thesis: contradiction
then 0 < ((UMP C) `2 ) - (lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U))) by XREAL_1:52;
then consider r being real number such that
A28: r in proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U) and
A29: r < (lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U))) + (((UMP C) `2 ) - (lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)))) by A20, A23, SEQ_4:def 5;
consider t being Point of (TOP-REAL 2) such that
A30: t in (LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U and
A31: proj2 . t = r by A28, Lm1;
A32: t `2 = r by A31, PSCOMP_1:def 29;
A33: (UMP C) `2 <= N-bound (L~ (Cage C,1)) by A21, A22, XXREAL_0:2;
t in LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]| by A30, XBOOLE_0:def 4;
hence contradiction by A4, A29, A32, A33, TOPREAL1:10; :: thesis: verum
end;
end;
end;
consider S', C' being Subset of (TopSpaceMetr (Euclid 2)) such that
A34: ( LSeg |[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]| = S' & C = C' ) and
A35: dist_min (LSeg |[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|),C = min_dist_min S',C' by JORDAN1K:def 1;
CC: ( S' is compact & C' is compact ) by A34, XX, COMPTS_1:33;
LSeg |[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]| misses C
proof
assume LSeg |[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]| meets C ; :: thesis: contradiction
then consider x being set such that
A36: x in LSeg |[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]| and
A37: x in C by XBOOLE_0:3;
reconsider x = x as Point of (TOP-REAL 2) by A36;
A38: x `2 <= N-bound C by A37, PSCOMP_1:71;
A39: lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)) <= x `2 by A4, A6, A24, A36, TOPREAL1:10;
then A40: (UMP C) `2 < x `2 by A26, XXREAL_0:2;
x `1 = ((W-bound C) + (E-bound C)) / 2 by A5, A7, A9, A36, SPPOL_1:def 3;
then x in LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| by A1, A2, A8, A38, A40, GOBOARD7:8;
then x in {(UMP C)} by A10, A37, XBOOLE_0:def 4;
hence contradiction by A26, A39, TARSKI:def 1; :: thesis: verum
end;
then dist_min (LSeg |[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|),C > 0 by A34, A35, CC, JGRAPH_1:55;
then (dist_min (LSeg |[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|),C) / 2 > 0 by XREAL_1:217;
then consider k being Element of NAT such that
A41: 1 < k and
A42: ( dist ((Gauge C,k) * 1,1),((Gauge C,k) * 1,2) < (dist_min (LSeg |[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|),C) / 2 & dist ((Gauge C,k) * 1,1),((Gauge C,k) * 2,1) < (dist_min (LSeg |[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|),C) / 2 ) by GOBRD14:21;
set f = Cage C,k;
set G = Gauge C,k;
A43: (dist ((Gauge C,k) * 1,1),((Gauge C,k) * (1 + 1),1)) + (dist ((Gauge C,k) * 1,1),((Gauge C,k) * 1,(1 + 1))) < ((dist_min (LSeg |[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|),C) / 2) + ((dist_min (LSeg |[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|),C) / 2) by A42, XREAL_1:10;
set s = UMP (Upper_Arc (L~ (Cage C,k)));
A44: (UMP (Upper_Arc (L~ (Cage C,k)))) `1 = ((W-bound C) + (E-bound C)) / 2 by A11;
A45: (UMP (Upper_Arc (L~ (Cage C,k)))) `2 <= N-bound (L~ (Cage C,k)) by JORDAN21:60;
N-bound (L~ (Cage C,k)) <= N-bound (L~ (Cage C,1)) by A41, JORDAN10:7;
then A46: (UMP (Upper_Arc (L~ (Cage C,k)))) `2 <= N-bound (L~ (Cage C,1)) by A45, XXREAL_0:2;
(UMP (Upper_Arc (L~ (Cage C,k)))) `2 in proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U) by A13, A41;
then lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)) <= (UMP (Upper_Arc (L~ (Cage C,k)))) `2 by A20, SEQ_4:def 5;
then A47: UMP (Upper_Arc (L~ (Cage C,k))) in LSeg |[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]| by A3, A4, A5, A6, A44, A46, GOBOARD7:8;
A48: Upper_Arc (L~ (Cage C,k)) c= L~ (Cage C,k) by JORDAN6:76;
UMP (Upper_Arc (L~ (Cage C,k))) in Upper_Arc (L~ (Cage C,k)) by JORDAN21:43;
then consider i being Element of NAT such that
A49: ( 1 <= i & i + 1 <= len (Cage C,k) ) and
A50: UMP (Upper_Arc (L~ (Cage C,k))) in LSeg (Cage C,k),i by A48, SPPOL_2:13;
right_cell (Cage C,k),i,(Gauge C,k) meets C by A49, JORDAN9:33;
then consider c being set such that
A51: c in right_cell (Cage C,k),i,(Gauge C,k) and
A52: c in C by XBOOLE_0:3;
reconsider c = c as Point of (TOP-REAL 2) by A52;
A53: Cage C,k is_sequence_on Gauge C,k by JORDAN9:def 1;
then consider i1, j1, i2, j2 being Element of NAT such that
A54: [i1,j1] in Indices (Gauge C,k) and
A55: (Cage C,k) /. i = (Gauge C,k) * i1,j1 and
A56: [i2,j2] in Indices (Gauge C,k) and
A57: (Cage C,k) /. (i + 1) = (Gauge C,k) * i2,j2 and
A58: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A49, JORDAN8:6;
(left_cell (Cage C,k),i,(Gauge C,k)) /\ (right_cell (Cage C,k),i,(Gauge C,k)) = LSeg (Cage C,k),i by A49, A53, GOBRD13:30;
then A59: UMP (Upper_Arc (L~ (Cage C,k))) in right_cell (Cage C,k),i,(Gauge C,k) by A50, XBOOLE_0:def 4;
A60: i1 + 1 <> i1 + 0 ;
A61: (i2 + 1) + 1 <> i2 ;
A62: (j2 + 1) + 1 <> j2 ;
A63: 1 <= i1 by A54, MATRIX_1:39;
A64: 1 <= j1 by A54, MATRIX_1:39;
A65: 1 <= i2 by A56, MATRIX_1:39;
A66: 1 <= j2 by A56, MATRIX_1:39;
A67: 1 <= i1 + 1 by NAT_1:11;
A68: 1 <= j1 + 1 by NAT_1:11;
A69: i1 <= len (Gauge C,k) by A54, MATRIX_1:39;
A70: j1 <= width (Gauge C,k) by A54, MATRIX_1:39;
A71: i2 <= len (Gauge C,k) by A56, MATRIX_1:39;
A72: j2 <= width (Gauge C,k) by A56, MATRIX_1:39;
reconsider s' = UMP (Upper_Arc (L~ (Cage C,k))), c' = c as Point of (Euclid 2) by EUCLID:71;
A73: min_dist_min S',C' <= dist s',c' by A34, A47, A52, XX, CC, WEIERSTR:40;
A74: dist s',c' = dist (UMP (Upper_Arc (L~ (Cage C,k)))),c by TOPREAL6:def 1;
[1,(1 + 1)] in Indices (Gauge C,k) by Th6;
then A75: dist ((Gauge C,k) * 1,1),((Gauge C,k) * 1,(1 + 1)) = ((N-bound C) - (S-bound C)) / (2 |^ k) by Th5, GOBRD14:19;
[(1 + 1),1] in Indices (Gauge C,k) by Th7;
then A76: dist ((Gauge C,k) * 1,1),((Gauge C,k) * (1 + 1),1) = ((E-bound C) - (W-bound C)) / (2 |^ k) by Th5, GOBRD14:20;
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 A58;
suppose A77: ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis: contradiction
then A78: j1 + 1 <= width (Gauge C,k) by A56, MATRIX_1:39;
i1 < len (Gauge C,k) by A49, A54, A55, A56, A57, A77, JORDAN10:1;
then A79: i1 + 1 <= len (Gauge C,k) by NAT_1:13;
right_cell (Cage C,k),i,(Gauge C,k) = cell (Gauge C,k),i1,j1 by A49, A53, A54, A55, A56, A57, A60, A62, A77, GOBRD13:def 2;
then ( ((Gauge C,k) * i1,j1) `1 <= c `1 & c `1 <= ((Gauge C,k) * (i1 + 1),j1) `1 & ((Gauge C,k) * i1,j1) `2 <= c `2 & c `2 <= ((Gauge C,k) * i1,(j1 + 1)) `2 & ((Gauge C,k) * i1,j1) `1 <= (UMP (Upper_Arc (L~ (Cage C,k)))) `1 & (UMP (Upper_Arc (L~ (Cage C,k)))) `1 <= ((Gauge C,k) * (i1 + 1),j1) `1 & ((Gauge C,k) * i1,j1) `2 <= (UMP (Upper_Arc (L~ (Cage C,k)))) `2 & (UMP (Upper_Arc (L~ (Cage C,k)))) `2 <= ((Gauge C,k) * i1,(j1 + 1)) `2 ) by A51, A59, A63, A64, A78, A79, JORDAN9:19;
then A80: dist (UMP (Upper_Arc (L~ (Cage C,k)))),c <= ((((Gauge C,k) * (i1 + 1),j1) `1 ) - (((Gauge C,k) * i1,j1) `1 )) + ((((Gauge C,k) * i1,(j1 + 1)) `2 ) - (((Gauge C,k) * i1,j1) `2 )) by TOPREAL6:104;
A81: [(i1 + 1),j1] in Indices (Gauge C,k) by A64, A67, A70, A79, MATRIX_1:37;
then A82: dist ((Gauge C,k) * i1,j1),((Gauge C,k) * (i1 + 1),j1) = (((Gauge C,k) * (i1 + 1),j1) `1 ) - (((Gauge C,k) * i1,j1) `1 ) by A54, GOBRD14:15;
A83: dist ((Gauge C,k) * i1,j1),((Gauge C,k) * i1,(j1 + 1)) = (((Gauge C,k) * i1,(j1 + 1)) `2 ) - (((Gauge C,k) * i1,j1) `2 ) by A54, A56, A77, GOBRD14:16;
A84: dist ((Gauge C,k) * i1,j1),((Gauge C,k) * i1,(j1 + 1)) = ((N-bound C) - (S-bound C)) / (2 |^ k) by A54, A56, A77, GOBRD14:19;
dist ((Gauge C,k) * i1,j1),((Gauge C,k) * (i1 + 1),j1) = ((E-bound C) - (W-bound C)) / (2 |^ k) by A54, A81, GOBRD14:20;
hence contradiction by A35, A43, A73, A74, A75, A76, A80, A82, A83, A84, XXREAL_0:2; :: thesis: verum
end;
suppose A85: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis: contradiction
then A86: i1 + 1 <= len (Gauge C,k) by A56, MATRIX_1:39;
1 < j1 by A49, A54, A55, A56, A57, A85, JORDAN10:3;
then A87: 1 <= j1 -' 1 by NAT_D:49;
A88: j1 -' 1 <= width (Gauge C,k) by A70, NAT_D:44;
A89: (j1 -' 1) + 1 = j1 by A87, NAT_D:43;
right_cell (Cage C,k),i,(Gauge C,k) = cell (Gauge C,k),i1,(j1 -' 1) by A49, A53, A54, A55, A56, A57, A60, A61, A85, GOBRD13:def 2;
then ( ((Gauge C,k) * i1,(j1 -' 1)) `1 <= c `1 & c `1 <= ((Gauge C,k) * (i1 + 1),(j1 -' 1)) `1 & ((Gauge C,k) * i1,(j1 -' 1)) `2 <= c `2 & c `2 <= ((Gauge C,k) * i1,((j1 -' 1) + 1)) `2 & ((Gauge C,k) * i1,(j1 -' 1)) `1 <= (UMP (Upper_Arc (L~ (Cage C,k)))) `1 & (UMP (Upper_Arc (L~ (Cage C,k)))) `1 <= ((Gauge C,k) * (i1 + 1),(j1 -' 1)) `1 & ((Gauge C,k) * i1,(j1 -' 1)) `2 <= (UMP (Upper_Arc (L~ (Cage C,k)))) `2 & (UMP (Upper_Arc (L~ (Cage C,k)))) `2 <= ((Gauge C,k) * i1,((j1 -' 1) + 1)) `2 ) by A51, A59, A63, A70, A86, A87, A89, JORDAN9:19;
then A90: dist (UMP (Upper_Arc (L~ (Cage C,k)))),c <= ((((Gauge C,k) * (i1 + 1),(j1 -' 1)) `1 ) - (((Gauge C,k) * i1,(j1 -' 1)) `1 )) + ((((Gauge C,k) * i1,((j1 -' 1) + 1)) `2 ) - (((Gauge C,k) * i1,(j1 -' 1)) `2 )) by TOPREAL6:104;
A91: [i1,(j1 -' 1)] in Indices (Gauge C,k) by A63, A69, A87, A88, MATRIX_1:37;
A92: [(i1 + 1),(j1 -' 1)] in Indices (Gauge C,k) by A65, A71, A85, A87, A88, MATRIX_1:37;
then A93: dist ((Gauge C,k) * i1,(j1 -' 1)),((Gauge C,k) * (i1 + 1),(j1 -' 1)) = (((Gauge C,k) * (i1 + 1),(j1 -' 1)) `1 ) - (((Gauge C,k) * i1,(j1 -' 1)) `1 ) by A91, GOBRD14:15;
A94: dist ((Gauge C,k) * i1,(j1 -' 1)),((Gauge C,k) * i1,((j1 -' 1) + 1)) = (((Gauge C,k) * i1,((j1 -' 1) + 1)) `2 ) - (((Gauge C,k) * i1,(j1 -' 1)) `2 ) by A54, A89, A91, GOBRD14:16;
A95: dist ((Gauge C,k) * i1,(j1 -' 1)),((Gauge C,k) * i1,((j1 -' 1) + 1)) = ((N-bound C) - (S-bound C)) / (2 |^ k) by A54, A89, A91, GOBRD14:19;
dist ((Gauge C,k) * i1,(j1 -' 1)),((Gauge C,k) * (i1 + 1),(j1 -' 1)) = ((E-bound C) - (W-bound C)) / (2 |^ k) by A91, A92, GOBRD14:20;
hence contradiction by A35, A43, A73, A74, A75, A76, A90, A93, A94, A95, XXREAL_0:2; :: thesis: verum
end;
suppose A96: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis: contradiction
then A97: i2 + 1 <= len (Gauge C,k) by A54, MATRIX_1:39;
j1 < width (Gauge C,k) by A49, A54, A55, A56, A57, A96, JORDAN10:4;
then A98: j1 + 1 <= width (Gauge C,k) by NAT_1:13;
right_cell (Cage C,k),i,(Gauge C,k) = cell (Gauge C,k),i2,j2 by A49, A53, A54, A55, A56, A57, A60, A61, A96, GOBRD13:def 2;
then ( ((Gauge C,k) * i2,j2) `1 <= c `1 & c `1 <= ((Gauge C,k) * (i2 + 1),j2) `1 & ((Gauge C,k) * i2,j2) `2 <= c `2 & c `2 <= ((Gauge C,k) * i2,(j2 + 1)) `2 & ((Gauge C,k) * i2,j2) `1 <= (UMP (Upper_Arc (L~ (Cage C,k)))) `1 & (UMP (Upper_Arc (L~ (Cage C,k)))) `1 <= ((Gauge C,k) * (i2 + 1),j2) `1 & ((Gauge C,k) * i2,j2) `2 <= (UMP (Upper_Arc (L~ (Cage C,k)))) `2 & (UMP (Upper_Arc (L~ (Cage C,k)))) `2 <= ((Gauge C,k) * i2,(j2 + 1)) `2 ) by A51, A59, A64, A65, A96, A97, A98, JORDAN9:19;
then A99: dist (UMP (Upper_Arc (L~ (Cage C,k)))),c <= ((((Gauge C,k) * (i2 + 1),j2) `1 ) - (((Gauge C,k) * i2,j2) `1 )) + ((((Gauge C,k) * i2,(j2 + 1)) `2 ) - (((Gauge C,k) * i2,j2) `2 )) by TOPREAL6:104;
A100: dist ((Gauge C,k) * i2,j2),((Gauge C,k) * (i2 + 1),j2) = (((Gauge C,k) * (i2 + 1),j2) `1 ) - (((Gauge C,k) * i2,j2) `1 ) by A54, A56, A96, GOBRD14:15;
A101: [i2,(j2 + 1)] in Indices (Gauge C,k) by A65, A68, A71, A96, A98, MATRIX_1:37;
then A102: dist ((Gauge C,k) * i2,j2),((Gauge C,k) * i2,(j2 + 1)) = (((Gauge C,k) * i2,(j2 + 1)) `2 ) - (((Gauge C,k) * i2,j2) `2 ) by A56, GOBRD14:16;
A103: dist ((Gauge C,k) * i2,j2),((Gauge C,k) * i2,(j2 + 1)) = ((N-bound C) - (S-bound C)) / (2 |^ k) by A56, A101, GOBRD14:19;
dist ((Gauge C,k) * i2,j2),((Gauge C,k) * (i2 + 1),j2) = ((E-bound C) - (W-bound C)) / (2 |^ k) by A54, A56, A96, GOBRD14:20;
hence contradiction by A35, A43, A73, A74, A75, A76, A99, A100, A102, A103, XXREAL_0:2; :: thesis: verum
end;
suppose A104: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis: contradiction
then A105: j2 + 1 <= width (Gauge C,k) by A54, MATRIX_1:39;
1 < i1 by A49, A54, A55, A56, A57, A104, JORDAN10:2;
then A106: 1 <= i1 -' 1 by NAT_D:49;
A107: i1 -' 1 <= len (Gauge C,k) by A69, NAT_D:44;
A108: (i1 -' 1) + 1 = i1 by A106, NAT_D:43;
right_cell (Cage C,k),i,(Gauge C,k) = cell (Gauge C,k),(i1 -' 1),j2 by A49, A53, A54, A55, A56, A57, A60, A62, A104, GOBRD13:def 2;
then ( ((Gauge C,k) * (i1 -' 1),j2) `1 <= c `1 & c `1 <= ((Gauge C,k) * ((i1 -' 1) + 1),j2) `1 & ((Gauge C,k) * (i1 -' 1),j2) `2 <= c `2 & c `2 <= ((Gauge C,k) * (i1 -' 1),(j2 + 1)) `2 & ((Gauge C,k) * (i1 -' 1),j2) `1 <= (UMP (Upper_Arc (L~ (Cage C,k)))) `1 & (UMP (Upper_Arc (L~ (Cage C,k)))) `1 <= ((Gauge C,k) * ((i1 -' 1) + 1),j2) `1 & ((Gauge C,k) * (i1 -' 1),j2) `2 <= (UMP (Upper_Arc (L~ (Cage C,k)))) `2 & (UMP (Upper_Arc (L~ (Cage C,k)))) `2 <= ((Gauge C,k) * (i1 -' 1),(j2 + 1)) `2 ) by A51, A59, A66, A69, A105, A106, A108, JORDAN9:19;
then A109: dist (UMP (Upper_Arc (L~ (Cage C,k)))),c <= ((((Gauge C,k) * ((i1 -' 1) + 1),j2) `1 ) - (((Gauge C,k) * (i1 -' 1),j2) `1 )) + ((((Gauge C,k) * (i1 -' 1),(j2 + 1)) `2 ) - (((Gauge C,k) * (i1 -' 1),j2) `2 )) by TOPREAL6:104;
A110: [(i1 -' 1),j2] in Indices (Gauge C,k) by A66, A72, A106, A107, MATRIX_1:37;
A111: [((i1 -' 1) + 1),j2] in Indices (Gauge C,k) by A63, A66, A69, A72, A108, MATRIX_1:37;
then A112: dist ((Gauge C,k) * (i1 -' 1),j2),((Gauge C,k) * ((i1 -' 1) + 1),j2) = (((Gauge C,k) * ((i1 -' 1) + 1),j2) `1 ) - (((Gauge C,k) * (i1 -' 1),j2) `1 ) by A110, GOBRD14:15;
A113: [(i1 -' 1),(j2 + 1)] in Indices (Gauge C,k) by A64, A70, A104, A106, A107, MATRIX_1:37;
then A114: dist ((Gauge C,k) * (i1 -' 1),j2),((Gauge C,k) * (i1 -' 1),(j2 + 1)) = (((Gauge C,k) * (i1 -' 1),(j2 + 1)) `2 ) - (((Gauge C,k) * (i1 -' 1),j2) `2 ) by A110, GOBRD14:16;
A115: dist ((Gauge C,k) * (i1 -' 1),j2),((Gauge C,k) * (i1 -' 1),(j2 + 1)) = ((N-bound C) - (S-bound C)) / (2 |^ k) by A110, A113, GOBRD14:19;
dist ((Gauge C,k) * (i1 -' 1),j2),((Gauge C,k) * ((i1 -' 1) + 1),j2) = ((E-bound C) - (W-bound C)) / (2 |^ k) by A110, A111, GOBRD14:20;
hence contradiction by A35, A43, A73, A74, A75, A76, A109, A112, A114, A115, XXREAL_0:2; :: thesis: verum
end;
end;
end;
hence UMP C in North_Arc C ; :: thesis: verum
end;
suppose UMP C = |[(((W-bound C) + (E-bound C)) / 2),(lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)))]| ; :: thesis: UMP C in North_Arc C
then A116: (UMP C) `2 = lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)) by EUCLID:56;
A117: North_Arc C = Lim_inf (Upper_Appr C) by JORDAN19:def 3;
ex S being Real_Sequence of 2 st
( S is convergent & ( for x being Element of NAT holds S . x in (Upper_Appr C) . x ) & UMP C = lim S )
proof
set R = { ((UMP (Upper_Arc (L~ (Cage C,n)))) `2 ) where n is Element of NAT : 0 < n } ;
{ ((UMP (Upper_Arc (L~ (Cage C,n)))) `2 ) where n is Element of NAT : 0 < n } c= REAL
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { ((UMP (Upper_Arc (L~ (Cage C,n)))) `2 ) where n is Element of NAT : 0 < n } or x in REAL )
assume x in { ((UMP (Upper_Arc (L~ (Cage C,n)))) `2 ) where n is Element of NAT : 0 < n } ; :: thesis: x in REAL
then ex n being Element of NAT st
( x = (UMP (Upper_Arc (L~ (Cage C,n)))) `2 & 0 < n ) ;
hence x in REAL ; :: thesis: verum
end;
then reconsider R = { ((UMP (Upper_Arc (L~ (Cage C,n)))) `2 ) where n is Element of NAT : 0 < n } as Subset of REAL ;
A118: (UMP (Upper_Arc (L~ (Cage C,1)))) `2 in R ;
A119: R is bounded_below
proof
take lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)) ; :: according to SEQ_4:def 2 :: thesis: for b1 being set holds
( not b1 in R or lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)) <= b1 )
let r be real number ; :: thesis: ( not r in R or lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)) <= r )
assume r in R ; :: thesis: lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)) <= r
then ex n being Element of NAT st
( r = (UMP (Upper_Arc (L~ (Cage C,n)))) `2 & 0 < n ) ;
then r in proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U) by A13;
hence lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)) <= r by A20, SEQ_4:def 5; :: thesis: verum
end;
deffunc H1( Element of NAT ) -> Element of the carrier of (TOP-REAL 2) = UMP (Upper_Arc (L~ (Cage C,$1)));
XX: for x being Element of NAT holds H1(x) is Element of REAL 2 by EUCLID:25;
consider S being Function of NAT ,(REAL 2) such that
A120: for n being Element of NAT holds S . n = H1(n) from FUNCT_2:sch 9(XX);
 the carrier of (TOP-REAL 2) = REAL 2 by EUCLID:25;
then reconsider SS = S as Real_Sequence of 2 by EUCLID:25;
take SS ; :: thesis: ( SS is convergent & ( for x being Element of NAT holds SS . x in (Upper_Appr C) . x ) & UMP C = lim SS )
reconsider pp = UMP C as Element of REAL 2 by EUCLID:25;
reconsider p1 = UMP C as Element of (TOP-REAL 2) ;
A121: for r being Real st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((S . m) - pp).| < r
proof
let r be Real; :: thesis: ( 0 < r implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((S . m) - pp).| < r )
assume A122: 0 < r ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((S . m) - pp).| < r
A123: for r being real number st r in R holds
lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)) <= r
proof
let r be real number ; :: thesis: ( r in R implies lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)) <= r )
assume r in R ; :: thesis: lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)) <= r
then ex n being Element of NAT st
( r = (UMP (Upper_Arc (L~ (Cage C,n)))) `2 & 0 < n ) ;
then r in proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U) by A13;
hence lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)) <= r by A20, SEQ_4:def 5; :: thesis: verum
end;
for s being real number st 0 < s holds
ex r being real number st
( r in R & r < (lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U))) + s )
proof
let s be real number ; :: thesis: ( 0 < s implies ex r being real number st
( r in R & r < (lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U))) + s ) )
assume 0 < s ; :: thesis: ex r being real number st
( r in R & r < (lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U))) + s )
then consider r being real number such that
A124: r in proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U) and
A125: r < (lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U))) + s by A20, A23, SEQ_4:def 5;
take r ; :: thesis: ( r in R & r < (lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U))) + s )
consider x being Point of (TOP-REAL 2) such that
A126: x in (LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U and
A127: proj2 . x = r by A124, Lm1;
x in U by A126, XBOOLE_0:def 4;
then consider n being Element of NAT such that
A128: x = UMP (Upper_Arc (L~ (Cage C,n))) and
A129: 0 < n ;
r = (UMP (Upper_Arc (L~ (Cage C,n)))) `2 by A127, A128, PSCOMP_1:def 29;
hence ( r in R & r < (lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U))) + s ) by A125, A129; :: thesis: verum
end;
then A130: inf R = lower_bound (proj2 .: ((LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|) /\ U)) by A118, A119, A123, SEQ_4:def 5;
consider v being real number such that
A131: v in R and
A132: v < (inf R) + r by A118, A119, A122, SEQ_4:def 5;
A133: v - (lower_bound R) < ((inf R) + r) - (inf R) by A132, XREAL_1:16;
consider n being Element of NAT such that
A134: v = (UMP (Upper_Arc (L~ (Cage C,n)))) `2 and
A135: 0 < n by A131;
take n ; :: thesis: for m being Element of NAT st n <= m holds
|.((S . m) - pp).| < r
let m be Element of NAT ; :: thesis: ( n <= m implies |.((S . m) - pp).| < r )
A136: S . m = UMP (Upper_Arc (L~ (Cage C,m))) by A120;
reconsider Sm = S . m as Element of (TOP-REAL 2) by EUCLID:25;
assume A137: n <= m ; :: thesis: |.((S . m) - pp).| < r
then (UMP (Upper_Arc (L~ (Cage C,m)))) `2 <= (UMP (Upper_Arc (L~ (Cage C,n)))) `2 by A135, Th29;
then Sm `2 <= v by A120, A134;
then (Sm `2 ) - ((UMP C) `2 ) <= v - ((UMP C) `2 ) by XREAL_1:15;
then A138: (Sm `2 ) - ((UMP C) `2 ) < r by A116, A130, A133, XXREAL_0:2;
A139: 0 < (Sm `2 ) - ((UMP C) `2 ) by A135, A136, A137, Th25, XREAL_1:52;
reconsider SSm = Sm as Point of (TOP-REAL 2) by EUCLID:25;
Q: SSm - p1 = (S . m) - pp by EUCLID:73;
Sm `1 = ((W-bound C) + (E-bound C)) / 2 by A11, A136;
then abs ((Sm `1 ) - ((UMP C) `1 )) = 0 by A8, ABSVALUE:def 1;
then |.((S . m) - pp).| <= 0 + (abs ((Sm `2 ) - ((UMP C) `2 ))) by Q, JGRAPH_1:49;
then |.((S . m) - pp).| <= (Sm `2 ) - ((UMP C) `2 ) by A139, ABSVALUE:def 1;
hence |.((S . m) - pp).| < r by A138, XXREAL_0:2; :: thesis: verum
end;
thus A140: SS is convergent :: thesis: ( ( for x being Element of NAT holds SS . x in (Upper_Appr C) . x ) & UMP C = lim SS )
proof
take UMP C ; :: according to TOPRNS_1:def 9 :: thesis: for b1 being Element of REAL holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= |.((SS . b3) - (UMP C)).| ) )
let r be Real; :: thesis: ( r <= 0 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not r <= |.((SS . b2) - (UMP C)).| ) )
assume Z: 0 < r ; :: thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not r <= |.((SS . b2) - (UMP C)).| )
then consider n being Element of NAT such that
W: for m being Element of NAT st n <= m holds
|.((S . m) - pp).| < r by A121;
take n ; :: thesis: for b1 being Element of NAT holds
( not n <= b1 or not r <= |.((SS . b1) - (UMP C)).| )
let m be Element of NAT ; :: thesis: ( not n <= m or not r <= |.((SS . m) - (UMP C)).| )
assume n <= m ; :: thesis: not r <= |.((SS . m) - (UMP C)).|
then |.((S . m) - pp).| < r by W;
hence |.((SS . m) - (UMP C)).| < r by EUCLID:73; :: thesis: verum
end;
hereby :: thesis: UMP C = lim SS
let x be Element of NAT ; :: thesis: SS . x in (Upper_Appr C) . x
A141: S . x = UMP (Upper_Arc (L~ (Cage C,x))) by A120;
(Upper_Appr C) . x = Upper_Arc (L~ (Cage C,x)) by JORDAN19:def 1;
hence SS . x in (Upper_Appr C) . x by A141, JORDAN21:43; :: thesis: verum
end;
for r being Real st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((SS . m) - (UMP C)).| < r
proof
let r be Real; :: thesis: ( 0 < r implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((SS . m) - (UMP C)).| < r )
assume Z: 0 < r ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((SS . m) - (UMP C)).| < r
then consider n being Element of NAT such that
W: for m being Element of NAT st n <= m holds
|.((S . m) - pp).| < r by A121;
take n ; :: thesis: for m being Element of NAT st n <= m holds
|.((SS . m) - (UMP C)).| < r
let m be Element of NAT ; :: thesis: ( n <= m implies |.((SS . m) - (UMP C)).| < r )
assume n <= m ; :: thesis: |.((SS . m) - (UMP C)).| < r
then |.((S . m) - pp).| < r by W;
hence |.((SS . m) - (UMP C)).| < r by EUCLID:73; :: thesis: verum
end;
hence UMP C = lim SS by A121, A140, TOPRNS_1:def 10; :: thesis: verum
end;
hence UMP C in North_Arc C by A117, KURATO_2:56; :: thesis: verum
end;
end;