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 Nat : 0 < n } ;
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))))]|);
A1: |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
A2: |[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]| `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
{ (UMP (Upper_Arc (L~ (Cage (C,n))))) where n is Nat : 0 < n } c= the carrier of (TOP-REAL 2)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (UMP (Upper_Arc (L~ (Cage (C,n))))) where n is 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 Nat : 0 < n } ; :: thesis: x in the carrier of (TOP-REAL 2)
then ex n being 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 Nat : 0 < n } as Subset of (TOP-REAL 2) ;
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))))]|);
A3: |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 = N-bound C by EUCLID:52;
A4: |[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]| `2 = N-bound (L~ (Cage (C,1))) by EUCLID:52;
A5: for n being Nat holds (UMP (Upper_Arc (L~ (Cage (C,n))))) `1 = ((W-bound C) + (E-bound C)) / 2
proof
let n be Nat; :: thesis: (UMP (Upper_Arc (L~ (Cage (C,n))))) `1 = ((W-bound C) + (E-bound C)) / 2
A6: (W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n)))) = (W-bound C) + (E-bound C) by JORDAN1G:33;
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:52
.= ((W-bound (L~ (Cage (C,n)))) + (E-bound (Upper_Arc (L~ (Cage (C,n)))))) / 2 by JORDAN21:17
.= ((W-bound C) + (E-bound C)) / 2 by A6, JORDAN21:18 ; :: thesis: verum
end;
A7: (UMP C) `2 <= (UMP (Upper_Arc (L~ (Cage (C,1))))) `2 by Th23;
A8: (LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|)) /\ C = {(UMP C)} by JORDAN21:34;
A9: (UMP (Upper_Arc (L~ (Cage (C,1))))) `2 <= N-bound (L~ (Cage (C,1))) by JORDAN21:47;
(LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U is bounded by TOPREAL6:89;
then proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U) is real-bounded by JCT_MISC:14;
then A10: proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U) is bounded_below ;
A11: (UMP C) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
A12: for n being 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 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))));
assume A13: 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 A14: UMP (Upper_Arc (L~ (Cage (C,n)))) in U ;
0 + 1 <= n by A13, NAT_1:13;
then ( 1 < n or n = 1 ) by XXREAL_0:1;
then A15: N-bound (L~ (Cage (C,n))) <= N-bound (L~ (Cage (C,1))) by JORDAN10:7;
(UMP (Upper_Arc (L~ (Cage (C,n))))) `2 <= N-bound (L~ (Cage (C,n))) by JORDAN21:47;
then A16: (UMP (Upper_Arc (L~ (Cage (C,n))))) `2 <= N-bound (L~ (Cage (C,1))) by A15, XXREAL_0:2;
A17: (UMP (Upper_Arc (L~ (Cage (C,n))))) `1 = ((W-bound C) + (E-bound C)) / 2 by A5;
(UMP C) `2 <= (UMP (Upper_Arc (L~ (Cage (C,n))))) `2 by A13, Th23;
then 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 A2, A4, A11, A16, A17, GOBOARD7:7;
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))))]|)) /\ U by A14, XBOOLE_0:def 4;
(UMP (Upper_Arc (L~ (Cage (C,n))))) `2 = proj2 . (UMP (Upper_Arc (L~ (Cage (C,n))))) by PSCOMP_1:def 6;
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 A18, FUNCT_2:35; :: thesis: verum
end;
then A19: (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) ;
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 A10, SEQ_4:def 2;
then A20: 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 A9, XXREAL_0:2;
A21: |[(((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:52;
then A22: 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 A2, SPPOL_1:16;
A23: |[(((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:68;
A24: |[(((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:52;
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
consider S9, C9 being Subset of (TopSpaceMetr (Euclid 2)) such that
A26: 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))))]|) = S9 and
A27: C = C9 and
A28: 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 (S9,C9) by JORDAN1K:def 1;
A29: S9 is compact by A26, Lm4, COMPTS_1:23;
A30: C9 is compact by A27, Lm4, COMPTS_1:23;
A31: now :: thesis: not (UMP C) `2 >= lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U))
assume A32: (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 A32, 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:52; :: 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:50;
then consider r being Real such that
A33: r in proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U) and
A34: 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 A10, A19, SEQ_4:def 2;
consider t being Point of (TOP-REAL 2) such that
A35: t in (LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U and
A36: proj2 . t = r by A33, Lm1;
A37: t in LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|) by A35, XBOOLE_0:def 4;
A38: (UMP C) `2 <= N-bound (L~ (Cage (C,1))) by A9, A7, XXREAL_0:2;
t `2 = r by A36, PSCOMP_1:def 6;
hence contradiction by A4, A34, A38, A37, TOPREAL1:4; :: thesis: verum
end;
end;
end;
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 object such that
A39: 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
A40: x in C by XBOOLE_0:3;
reconsider x = x as Point of (TOP-REAL 2) by A39;
A41: x `2 <= N-bound C by A40, PSCOMP_1:24;
A42: x `1 = ((W-bound C) + (E-bound C)) / 2 by A21, A23, A22, A39, SPPOL_1:def 3;
A43: lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)) <= x `2 by A4, A24, A20, A39, TOPREAL1:4;
then (UMP C) `2 < x `2 by A31, XXREAL_0:2;
then x in LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|) by A1, A3, A11, A41, A42, GOBOARD7:7;
then x in {(UMP C)} by A8, A40, XBOOLE_0:def 4;
hence contradiction by A31, A43, 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 A26, A27, A28, A29, A30, JGRAPH_1:38;
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 ;
then consider k being Nat such that
A44: 1 < k and
A45: 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 and
A46: 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:11;
set f = Cage (C,k);
set G = Gauge (C,k);
set s = UMP (Upper_Arc (L~ (Cage (C,k))));
A47: (UMP (Upper_Arc (L~ (Cage (C,k))))) `2 <= N-bound (L~ (Cage (C,k))) by JORDAN21:47;
A48: (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 A45, A46, XREAL_1:8;
N-bound (L~ (Cage (C,k))) <= N-bound (L~ (Cage (C,1))) by A44, JORDAN10:7;
then A49: (UMP (Upper_Arc (L~ (Cage (C,k))))) `2 <= N-bound (L~ (Cage (C,1))) by A47, 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 A12, A44;
then A50: 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 A10, SEQ_4:def 2;
[1,(1 + 1)] in Indices (Gauge (C,k)) by Th6;
then A51: dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,(1 + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ k) by Th5, GOBRD14:9;
[(1 + 1),1] in Indices (Gauge (C,k)) by Th7;
then A52: dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * ((1 + 1),1))) = ((E-bound C) - (W-bound C)) / (2 |^ k) by Th5, GOBRD14:10;
A53: UMP (Upper_Arc (L~ (Cage (C,k)))) in Upper_Arc (L~ (Cage (C,k))) by JORDAN21:30;
Upper_Arc (L~ (Cage (C,k))) c= L~ (Cage (C,k)) by JORDAN6:61;
then consider i being Nat such that
A54: 1 <= i and
A55: i + 1 <= len (Cage (C,k)) and
A56: UMP (Upper_Arc (L~ (Cage (C,k)))) in LSeg ((Cage (C,k)),i) by A53, SPPOL_2:13;
A57: Cage (C,k) is_sequence_on Gauge (C,k) by JORDAN9:def 1;
then consider i1, j1, i2, j2 being Nat such that
A58: [i1,j1] in Indices (Gauge (C,k)) and
A59: (Cage (C,k)) /. i = (Gauge (C,k)) * (i1,j1) and
A60: [i2,j2] in Indices (Gauge (C,k)) and
A61: (Cage (C,k)) /. (i + 1) = (Gauge (C,k)) * (i2,j2) and
A62: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A54, A55, JORDAN8:3;
A63: 1 <= i1 by A58, MATRIX_0:32;
right_cell ((Cage (C,k)),i,(Gauge (C,k))) meets C by A54, A55, JORDAN9:31;
then consider c being object such that
A64: c in right_cell ((Cage (C,k)),i,(Gauge (C,k))) and
A65: c in C by XBOOLE_0:3;
reconsider c = c as Point of (TOP-REAL 2) by A65;
reconsider s9 = UMP (Upper_Arc (L~ (Cage (C,k)))), c9 = c as Point of (Euclid 2) by EUCLID:67;
(UMP (Upper_Arc (L~ (Cage (C,k))))) `1 = ((W-bound C) + (E-bound C)) / 2 by A5;
then 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 A2, A4, A21, A24, A49, A50, GOBOARD7:7;
then A66: min_dist_min (S9,C9) <= dist (s9,c9) by A26, A27, A29, A30, A65, WEIERSTR:34;
A67: dist (s9,c9) = dist ((UMP (Upper_Arc (L~ (Cage (C,k))))),c) by TOPREAL6:def 1;
A68: 1 <= j2 by A60, MATRIX_0:32;
(left_cell ((Cage (C,k)),i,(Gauge (C,k)))) /\ (right_cell ((Cage (C,k)),i,(Gauge (C,k)))) = LSeg ((Cage (C,k)),i) by A54, A55, A57, GOBRD13:29;
then A69: UMP (Upper_Arc (L~ (Cage (C,k)))) in right_cell ((Cage (C,k)),i,(Gauge (C,k))) by A56, XBOOLE_0:def 4;
A70: j2 <= width (Gauge (C,k)) by A60, MATRIX_0:32;
A71: (j2 + 1) + 1 <> j2 ;
A72: 1 <= i2 by A60, MATRIX_0:32;
A73: j1 <= width (Gauge (C,k)) by A58, MATRIX_0:32;
A74: 1 <= j1 + 1 by NAT_1:11;
A75: i1 + 1 <> i1 + 0 ;
A76: i1 <= len (Gauge (C,k)) by A58, MATRIX_0:32;
A77: i2 <= len (Gauge (C,k)) by A60, MATRIX_0:32;
A78: (i2 + 1) + 1 <> i2 ;
A79: 1 <= j1 by A58, MATRIX_0:32;
A80: 1 <= i1 + 1 by NAT_1:11;
now :: thesis: contradiction
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 A62;
suppose A81: ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis: contradiction
then A82: dist (((Gauge (C,k)) * (i1,j1)),((Gauge (C,k)) * (i1,(j1 + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ k) by A58, A60, GOBRD14:9;
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 A58, A60, A81, GOBRD14:6;
i1 < len (Gauge (C,k)) by A54, A55, A58, A59, A60, A61, A81, JORDAN10:1;
then A84: i1 + 1 <= len (Gauge (C,k)) by NAT_1:13;
then A85: [(i1 + 1),j1] in Indices (Gauge (C,k)) by A79, A80, A73, MATRIX_0:30;
then A86: 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 A58, GOBRD14:5;
A87: dist (((Gauge (C,k)) * (i1,j1)),((Gauge (C,k)) * ((i1 + 1),j1))) = ((E-bound C) - (W-bound C)) / (2 |^ k) by A58, A85, GOBRD14:10;
A88: j1 + 1 <= width (Gauge (C,k)) by A60, A81, MATRIX_0:32;
A89: right_cell ((Cage (C,k)),i,(Gauge (C,k))) = cell ((Gauge (C,k)),i1,j1) by A54, A55, A57, A58, A59, A60, A61, A75, A71, A81, GOBRD13:def 2;
then A90: c `1 <= ((Gauge (C,k)) * ((i1 + 1),j1)) `1 by A64, A63, A79, A88, A84, JORDAN9:17;
A91: (UMP (Upper_Arc (L~ (Cage (C,k))))) `2 <= ((Gauge (C,k)) * (i1,(j1 + 1))) `2 by A69, A63, A79, A88, A84, A89, JORDAN9:17;
A92: ((Gauge (C,k)) * (i1,j1)) `2 <= (UMP (Upper_Arc (L~ (Cage (C,k))))) `2 by A69, A63, A79, A88, A84, A89, JORDAN9:17;
A93: (UMP (Upper_Arc (L~ (Cage (C,k))))) `1 <= ((Gauge (C,k)) * ((i1 + 1),j1)) `1 by A69, A63, A79, A88, A84, A89, JORDAN9:17;
A94: ((Gauge (C,k)) * (i1,j1)) `1 <= (UMP (Upper_Arc (L~ (Cage (C,k))))) `1 by A69, A63, A79, A88, A84, A89, JORDAN9:17;
A95: c `2 <= ((Gauge (C,k)) * (i1,(j1 + 1))) `2 by A64, A63, A79, A88, A84, A89, JORDAN9:17;
A96: ((Gauge (C,k)) * (i1,j1)) `2 <= c `2 by A64, A63, A79, A88, A84, A89, JORDAN9:17;
((Gauge (C,k)) * (i1,j1)) `1 <= c `1 by A64, A63, A79, A88, A84, A89, JORDAN9:17;
then 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 A90, A96, A95, A94, A93, A92, A91, TOPREAL6:95;
hence contradiction by A28, A48, A66, A67, A51, A52, A86, A83, A82, A87, XXREAL_0:2; :: thesis: verum
end;
suppose A97: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis: contradiction
then 1 < j1 by A54, A55, A58, A59, A60, A61, JORDAN10:3;
then A98: 1 <= j1 -' 1 by NAT_D:49;
then A99: (j1 -' 1) + 1 = j1 by NAT_D:43;
A100: j1 -' 1 <= width (Gauge (C,k)) by A73, NAT_D:44;
then A101: [i1,(j1 -' 1)] in Indices (Gauge (C,k)) by A63, A76, A98, MATRIX_0:30;
then A102: 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 A58, A99, GOBRD14:6;
A103: [(i1 + 1),(j1 -' 1)] in Indices (Gauge (C,k)) by A72, A77, A97, A98, A100, MATRIX_0:30;
then A104: 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 A101, GOBRD14:5;
A105: dist (((Gauge (C,k)) * (i1,(j1 -' 1))),((Gauge (C,k)) * (i1,((j1 -' 1) + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ k) by A58, A99, A101, GOBRD14:9;
A106: dist (((Gauge (C,k)) * (i1,(j1 -' 1))),((Gauge (C,k)) * ((i1 + 1),(j1 -' 1)))) = ((E-bound C) - (W-bound C)) / (2 |^ k) by A101, A103, GOBRD14:10;
A107: i1 + 1 <= len (Gauge (C,k)) by A60, A97, MATRIX_0:32;
A108: right_cell ((Cage (C,k)),i,(Gauge (C,k))) = cell ((Gauge (C,k)),i1,(j1 -' 1)) by A54, A55, A57, A58, A59, A60, A61, A75, A78, A97, GOBRD13:def 2;
then A109: c `1 <= ((Gauge (C,k)) * ((i1 + 1),(j1 -' 1))) `1 by A64, A63, A73, A107, A98, A99, JORDAN9:17;
A110: (UMP (Upper_Arc (L~ (Cage (C,k))))) `2 <= ((Gauge (C,k)) * (i1,((j1 -' 1) + 1))) `2 by A69, A63, A73, A107, A98, A99, A108, JORDAN9:17;
A111: ((Gauge (C,k)) * (i1,(j1 -' 1))) `2 <= (UMP (Upper_Arc (L~ (Cage (C,k))))) `2 by A69, A63, A73, A107, A98, A99, A108, JORDAN9:17;
A112: (UMP (Upper_Arc (L~ (Cage (C,k))))) `1 <= ((Gauge (C,k)) * ((i1 + 1),(j1 -' 1))) `1 by A69, A63, A73, A107, A98, A99, A108, JORDAN9:17;
A113: ((Gauge (C,k)) * (i1,(j1 -' 1))) `1 <= (UMP (Upper_Arc (L~ (Cage (C,k))))) `1 by A69, A63, A73, A107, A98, A99, A108, JORDAN9:17;
A114: c `2 <= ((Gauge (C,k)) * (i1,((j1 -' 1) + 1))) `2 by A64, A63, A73, A107, A98, A99, A108, JORDAN9:17;
A115: ((Gauge (C,k)) * (i1,(j1 -' 1))) `2 <= c `2 by A64, A63, A73, A107, A98, A99, A108, JORDAN9:17;
((Gauge (C,k)) * (i1,(j1 -' 1))) `1 <= c `1 by A64, A63, A73, A107, A98, A99, A108, JORDAN9:17;
then 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 A109, A115, A114, A113, A112, A111, A110, TOPREAL6:95;
hence contradiction by A28, A48, A66, A67, A51, A52, A104, A102, A105, A106, XXREAL_0:2; :: thesis: verum
end;
suppose A116: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis: contradiction
then A117: dist (((Gauge (C,k)) * (i2,j2)),((Gauge (C,k)) * ((i2 + 1),j2))) = ((E-bound C) - (W-bound C)) / (2 |^ k) by A58, A60, GOBRD14:10;
A118: 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 A58, A60, A116, GOBRD14:5;
A119: i2 + 1 <= len (Gauge (C,k)) by A58, A116, MATRIX_0:32;
j1 < width (Gauge (C,k)) by A54, A55, A58, A59, A60, A61, A116, JORDAN10:4;
then A120: j1 + 1 <= width (Gauge (C,k)) by NAT_1:13;
then A121: [i2,(j2 + 1)] in Indices (Gauge (C,k)) by A72, A74, A77, A116, MATRIX_0:30;
then A122: 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 A60, GOBRD14:6;
A123: right_cell ((Cage (C,k)),i,(Gauge (C,k))) = cell ((Gauge (C,k)),i2,j2) by A54, A55, A57, A58, A59, A60, A61, A75, A78, A116, GOBRD13:def 2;
then A124: c `1 <= ((Gauge (C,k)) * ((i2 + 1),j2)) `1 by A64, A79, A72, A116, A119, A120, JORDAN9:17;
A125: (UMP (Upper_Arc (L~ (Cage (C,k))))) `2 <= ((Gauge (C,k)) * (i2,(j2 + 1))) `2 by A69, A79, A72, A116, A119, A120, A123, JORDAN9:17;
A126: ((Gauge (C,k)) * (i2,j2)) `2 <= c `2 by A64, A79, A72, A116, A119, A120, A123, JORDAN9:17;
A127: dist (((Gauge (C,k)) * (i2,j2)),((Gauge (C,k)) * (i2,(j2 + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ k) by A60, A121, GOBRD14:9;
A128: ((Gauge (C,k)) * (i2,j2)) `2 <= (UMP (Upper_Arc (L~ (Cage (C,k))))) `2 by A69, A79, A72, A116, A119, A120, A123, JORDAN9:17;
A129: (UMP (Upper_Arc (L~ (Cage (C,k))))) `1 <= ((Gauge (C,k)) * ((i2 + 1),j2)) `1 by A69, A79, A72, A116, A119, A120, A123, JORDAN9:17;
A130: ((Gauge (C,k)) * (i2,j2)) `1 <= (UMP (Upper_Arc (L~ (Cage (C,k))))) `1 by A69, A79, A72, A116, A119, A120, A123, JORDAN9:17;
A131: c `2 <= ((Gauge (C,k)) * (i2,(j2 + 1))) `2 by A64, A79, A72, A116, A119, A120, A123, JORDAN9:17;
((Gauge (C,k)) * (i2,j2)) `1 <= c `1 by A64, A79, A72, A116, A119, A120, A123, JORDAN9:17;
then 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 A124, A126, A131, A130, A129, A128, A125, TOPREAL6:95;
hence contradiction by A28, A48, A66, A67, A51, A52, A118, A122, A127, A117, XXREAL_0:2; :: thesis: verum
end;
suppose A132: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis: contradiction
then 1 < i1 by A54, A55, A58, A59, A60, A61, JORDAN10:2;
then A133: 1 <= i1 -' 1 by NAT_D:49;
A134: i1 -' 1 <= len (Gauge (C,k)) by A76, NAT_D:44;
then A135: [(i1 -' 1),j2] in Indices (Gauge (C,k)) by A68, A70, A133, MATRIX_0:30;
A136: [(i1 -' 1),(j2 + 1)] in Indices (Gauge (C,k)) by A79, A73, A132, A133, A134, MATRIX_0:30;
then A137: 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 A135, GOBRD14:6;
A138: dist (((Gauge (C,k)) * ((i1 -' 1),j2)),((Gauge (C,k)) * ((i1 -' 1),(j2 + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ k) by A135, A136, GOBRD14:9;
A139: j2 + 1 <= width (Gauge (C,k)) by A58, A132, MATRIX_0:32;
A140: (i1 -' 1) + 1 = i1 by A133, NAT_D:43;
then A141: [((i1 -' 1) + 1),j2] in Indices (Gauge (C,k)) by A63, A68, A76, A70, MATRIX_0:30;
then A142: 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 A135, GOBRD14:5;
A143: right_cell ((Cage (C,k)),i,(Gauge (C,k))) = cell ((Gauge (C,k)),(i1 -' 1),j2) by A54, A55, A57, A58, A59, A60, A61, A75, A71, A132, GOBRD13:def 2;
then A144: c `1 <= ((Gauge (C,k)) * (((i1 -' 1) + 1),j2)) `1 by A64, A68, A76, A139, A133, A140, JORDAN9:17;
A145: (UMP (Upper_Arc (L~ (Cage (C,k))))) `2 <= ((Gauge (C,k)) * ((i1 -' 1),(j2 + 1))) `2 by A69, A68, A76, A139, A133, A140, A143, JORDAN9:17;
A146: ((Gauge (C,k)) * ((i1 -' 1),j2)) `2 <= (UMP (Upper_Arc (L~ (Cage (C,k))))) `2 by A69, A68, A76, A139, A133, A140, A143, JORDAN9:17;
A147: (UMP (Upper_Arc (L~ (Cage (C,k))))) `1 <= ((Gauge (C,k)) * (((i1 -' 1) + 1),j2)) `1 by A69, A68, A76, A139, A133, A140, A143, JORDAN9:17;
A148: ((Gauge (C,k)) * ((i1 -' 1),j2)) `1 <= (UMP (Upper_Arc (L~ (Cage (C,k))))) `1 by A69, A68, A76, A139, A133, A140, A143, JORDAN9:17;
A149: c `2 <= ((Gauge (C,k)) * ((i1 -' 1),(j2 + 1))) `2 by A64, A68, A76, A139, A133, A140, A143, JORDAN9:17;
A150: ((Gauge (C,k)) * ((i1 -' 1),j2)) `2 <= c `2 by A64, A68, A76, A139, A133, A140, A143, JORDAN9:17;
A151: dist (((Gauge (C,k)) * ((i1 -' 1),j2)),((Gauge (C,k)) * (((i1 -' 1) + 1),j2))) = ((E-bound C) - (W-bound C)) / (2 |^ k) by A135, A141, GOBRD14:10;
((Gauge (C,k)) * ((i1 -' 1),j2)) `1 <= c `1 by A64, A68, A76, A139, A133, A140, A143, JORDAN9:17;
then 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 A144, A150, A149, A148, A147, A146, A145, TOPREAL6:95;
hence contradiction by A28, A48, A66, A67, A51, A52, A142, A137, A138, A151, 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 A152: (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:52;
A153: ex S being Real_Sequence of 2 st
( S is convergent & ( for x being 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 Nat : 0 < n } ;
{ ((UMP (Upper_Arc (L~ (Cage (C,n))))) `2) where n is Nat : 0 < n } c= REAL
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ((UMP (Upper_Arc (L~ (Cage (C,n))))) `2) where n is Nat : 0 < n } or x in REAL )
assume x in { ((UMP (Upper_Arc (L~ (Cage (C,n))))) `2) where n is Nat : 0 < n } ; :: thesis: x in REAL
then ex n being Nat st
( x = (UMP (Upper_Arc (L~ (Cage (C,n))))) `2 & 0 < n ) ;
hence x in REAL by XREAL_0:def 1; :: thesis: verum
end;
then reconsider R = { ((UMP (Upper_Arc (L~ (Cage (C,n))))) `2) where n is Nat : 0 < n } as Subset of REAL ;
deffunc H1( Nat) -> Element of the carrier of (TOP-REAL 2) = UMP (Upper_Arc (L~ (Cage (C,$1))));
reconsider pp = UMP C as Element of REAL 2 by EUCLID:22;
reconsider p1 = UMP C as Element of (TOP-REAL 2) ;
A154: for x being Element of NAT holds H1(x) is Element of REAL 2 by EUCLID:22;
consider S being sequence of (REAL 2) such that
A155: for n being Element of NAT holds S . n = H1(n) from FUNCT_2:sch 9(A154);
 the carrier of (TOP-REAL 2) = REAL 2 by EUCLID:22;
then reconsider SS = S as Real_Sequence of 2 ;
take SS ; :: thesis: ( SS is convergent & ( for x being Nat holds SS . x in (Upper_Appr C) . x ) & UMP C = lim SS )
A156: 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 XXREAL_2:def 9 :: thesis: lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)) is LowerBound of R
let r be ExtReal; :: according to XXREAL_2:def 2 :: 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 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 A12;
hence lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)) <= r by A10, SEQ_4:def 2; :: thesis: verum
end;
A157: (UMP (Upper_Arc (L~ (Cage (C,1))))) `2 in R ;
A158: for r being Real st 0 < r holds
ex n being Nat st
for m being Nat st n <= m holds
|.((S . m) - pp).| < r
proof
A159: for s being Real st 0 < s holds
ex r being Real 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; :: thesis: ( 0 < s implies ex r being Real 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 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 such that
A160: r in proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U) and
A161: r < (lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U))) + s by A10, A19, SEQ_4:def 2;
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
A162: x in (LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U and
A163: proj2 . x = r by A160, Lm1;
x in U by A162, XBOOLE_0:def 4;
then consider n being Nat such that
A164: x = UMP (Upper_Arc (L~ (Cage (C,n)))) and
A165: 0 < n ;
r = (UMP (Upper_Arc (L~ (Cage (C,n))))) `2 by A163, A164, PSCOMP_1:def 6;
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 A161, A165; :: thesis: verum
end;
let r be Real; :: thesis: ( 0 < r implies ex n being Nat st
for m being Nat st n <= m holds
|.((S . m) - pp).| < r )
assume 0 < r ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((S . m) - pp).| < r
then consider v being Real such that
A166: v in R and
A167: v < (lower_bound R) + r by A157, A156, SEQ_4:def 2;
A168: v - (lower_bound R) < ((lower_bound R) + r) - (lower_bound R) by A167, XREAL_1:14;
consider n being Nat such that
A169: v = (UMP (Upper_Arc (L~ (Cage (C,n))))) `2 and
A170: 0 < n by A166;
take n ; :: thesis: for m being Nat st n <= m holds
|.((S . m) - pp).| < r
let m be Nat; :: thesis: ( n <= m implies |.((S . m) - pp).| < r )
reconsider Sm = S . m as Element of (TOP-REAL 2) by EUCLID:22;
A171: m in NAT by ORDINAL1:def 12;
assume A172: 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 A170, Th27;
then Sm `2 <= v by A155, A169, A171;
then A173: (Sm `2) - ((UMP C) `2) <= v - ((UMP C) `2) by XREAL_1:13;
reconsider SSm = Sm as Point of (TOP-REAL 2) ;
A174: SSm - p1 = (S . m) - pp ;
A175: S . m = UMP (Upper_Arc (L~ (Cage (C,m)))) by A155, A171;
then Sm `1 = ((W-bound C) + (E-bound C)) / 2 by A5;
then |.((Sm `1) - ((UMP C) `1)).| = 0 by A11, ABSVALUE:def 1;
then A176: |.((S . m) - pp).| <= 0 + |.((Sm `2) - ((UMP C) `2)).| by A174, JGRAPH_1:32;
0 < (Sm `2) - ((UMP C) `2) by A170, A175, A172, Th23, XREAL_1:50;
then A177: |.((S . m) - pp).| <= (Sm `2) - ((UMP C) `2) by A176, ABSVALUE:def 1;
for r being Real 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; :: 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 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 A12;
hence lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)) <= r by A10, SEQ_4:def 2; :: thesis: verum
end;
then lower_bound R = lower_bound (proj2 .: ((LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage (C,1))))]|)) /\ U)) by A157, A156, A159, SEQ_4:def 2;
then (Sm `2) - ((UMP C) `2) < r by A152, A168, A173, XXREAL_0:2;
hence |.((S . m) - pp).| < r by A177, XXREAL_0:2; :: thesis: verum
end;
thus A178: SS is convergent :: thesis: ( ( for x being Nat holds SS . x in (Upper_Appr C) . x ) & UMP C = lim SS )
proof
take UMP C ; :: according to TOPRNS_1:def 8 :: thesis: for b1 being object holds
( b1 <= 0 or ex b2 being set st
for b3 being set holds
( not b2 <= b3 or not b1 <= |.((SS . b3) - (UMP C)).| ) )
let r be Real; :: thesis: ( r <= 0 or ex b1 being set st
for b2 being set holds
( not b1 <= b2 or not r <= |.((SS . b2) - (UMP C)).| ) )
assume 0 < r ; :: thesis: ex b1 being set st
for b2 being set holds
( not b1 <= b2 or not r <= |.((SS . b2) - (UMP C)).| )
then consider n being Nat such that
A179: for m being Nat st n <= m holds
|.((S . m) - pp).| < r by A158;
take n ; :: thesis: for b1 being set holds
( not n <= b1 or not r <= |.((SS . b1) - (UMP C)).| )
let m be 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 A179;
hence |.((SS . m) - (UMP C)).| < r ; :: thesis: verum
end;
for r being Real st 0 < r holds
ex n being Nat st
for m being Nat st n <= m holds
|.((SS . m) - (UMP C)).| < r
proof
let r be Real; :: thesis: ( 0 < r implies ex n being Nat st
for m being Nat st n <= m holds
|.((SS . m) - (UMP C)).| < r )
assume 0 < r ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((SS . m) - (UMP C)).| < r
then consider n being Nat such that
A182: for m being Nat st n <= m holds
|.((S . m) - pp).| < r by A158;
take n ; :: thesis: for m being Nat st n <= m holds
|.((SS . m) - (UMP C)).| < r
let m be 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 A182;
hence |.((SS . m) - (UMP C)).| < r ; :: thesis: verum
end;
hence UMP C = lim SS by A178, TOPRNS_1:def 9; :: thesis: verum
end;
North_Arc C = Lim_inf (Upper_Appr C) by JORDAN19:def 3;
hence UMP C in North_Arc C by A153, KURATO_2:21; :: thesis: verum
end;
end;