:: JORDAN22 semantic presentation begin Lm1: for r being real number for X being Subset of (TOP-REAL 2) st r in proj2 .: X holds ex x being Point of (TOP-REAL 2) st ( x in X & proj2 . x = r ) proof let r be real number ; ::_thesis: for X being Subset of (TOP-REAL 2) st r in proj2 .: X holds ex x being Point of (TOP-REAL 2) st ( x in X & proj2 . x = r ) let X be Subset of (TOP-REAL 2); ::_thesis: ( r in proj2 .: X implies ex x being Point of (TOP-REAL 2) st ( x in X & proj2 . x = r ) ) assume r in proj2 .: X ; ::_thesis: ex x being Point of (TOP-REAL 2) st ( x in X & proj2 . x = r ) then ex x being set st ( x in the carrier of (TOP-REAL 2) & x in X & proj2 . x = r ) by FUNCT_2:64; hence ex x being Point of (TOP-REAL 2) st ( x in X & proj2 . x = r ) ; ::_thesis: verum end; theorem Th1: :: JORDAN22:1 for C being Simple_closed_curve for i being Element of NAT holds (Upper_Appr C) . i c= Cl (RightComp (Cage (C,0))) proof let C be Simple_closed_curve; ::_thesis: for i being Element of NAT holds (Upper_Appr C) . i c= Cl (RightComp (Cage (C,0))) let i be Element of NAT ; ::_thesis: (Upper_Appr C) . i c= Cl (RightComp (Cage (C,0))) A1: Upper_Arc (L~ (Cage (C,i))) c= L~ (Cage (C,i)) by JORDAN6:61; A2: L~ (Cage (C,i)) c= Cl (RightComp (Cage (C,0))) by JORDAN1H:46; (Upper_Appr C) . i = Upper_Arc (L~ (Cage (C,i))) by JORDAN19:def_1; hence (Upper_Appr C) . i c= Cl (RightComp (Cage (C,0))) by A1, A2, XBOOLE_1:1; ::_thesis: verum end; theorem Th2: :: JORDAN22:2 for C being Simple_closed_curve for i being Element of NAT holds (Lower_Appr C) . i c= Cl (RightComp (Cage (C,0))) proof let C be Simple_closed_curve; ::_thesis: for i being Element of NAT holds (Lower_Appr C) . i c= Cl (RightComp (Cage (C,0))) let i be Element of NAT ; ::_thesis: (Lower_Appr C) . i c= Cl (RightComp (Cage (C,0))) A1: Lower_Arc (L~ (Cage (C,i))) c= L~ (Cage (C,i)) by JORDAN6:61; A2: L~ (Cage (C,i)) c= Cl (RightComp (Cage (C,0))) by JORDAN1H:46; (Lower_Appr C) . i = Lower_Arc (L~ (Cage (C,i))) by JORDAN19:def_2; hence (Lower_Appr C) . i c= Cl (RightComp (Cage (C,0))) by A1, A2, XBOOLE_1:1; ::_thesis: verum end; registration let C be Simple_closed_curve; cluster Upper_Arc C -> connected ; coherence Upper_Arc C is connected proof Upper_Arc C is_an_arc_of W-min C, E-max C by JORDAN6:def_8; hence Upper_Arc C is connected by JORDAN6:10; ::_thesis: verum end; cluster Lower_Arc C -> connected ; coherence Lower_Arc C is connected proof Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:def_9; hence Lower_Arc C is connected by JORDAN6:10; ::_thesis: verum end; end; theorem :: JORDAN22:3 for C being Simple_closed_curve for i being Element of NAT holds ( (Upper_Appr C) . i is compact & (Upper_Appr C) . i is connected ) proof let C be Simple_closed_curve; ::_thesis: for i being Element of NAT holds ( (Upper_Appr C) . i is compact & (Upper_Appr C) . i is connected ) let i be Element of NAT ; ::_thesis: ( (Upper_Appr C) . i is compact & (Upper_Appr C) . i is connected ) Upper_Arc (L~ (Cage (C,i))) is compact ; hence (Upper_Appr C) . i is compact by JORDAN19:def_1; ::_thesis: (Upper_Appr C) . i is connected Upper_Arc (L~ (Cage (C,i))) is connected ; hence (Upper_Appr C) . i is connected by JORDAN19:def_1; ::_thesis: verum end; theorem :: JORDAN22:4 for C being Simple_closed_curve for i being Element of NAT holds ( (Lower_Appr C) . i is compact & (Lower_Appr C) . i is connected ) proof let C be Simple_closed_curve; ::_thesis: for i being Element of NAT holds ( (Lower_Appr C) . i is compact & (Lower_Appr C) . i is connected ) let i be Element of NAT ; ::_thesis: ( (Lower_Appr C) . i is compact & (Lower_Appr C) . i is connected ) Lower_Arc (L~ (Cage (C,i))) is compact ; hence (Lower_Appr C) . i is compact by JORDAN19:def_2; ::_thesis: (Lower_Appr C) . i is connected Lower_Arc (L~ (Cage (C,i))) is connected ; hence (Lower_Appr C) . i is connected by JORDAN19:def_2; ::_thesis: verum end; registration let C be Simple_closed_curve; cluster North_Arc C -> compact ; coherence North_Arc C is compact proof for i being Element of NAT holds (Upper_Appr C) . i c= Cl (RightComp (Cage (C,0))) by Th1; then Lim_inf (Upper_Appr C) is compact by KURATO_2:26; hence North_Arc C is compact by JORDAN19:def_3; ::_thesis: verum end; cluster South_Arc C -> compact ; coherence South_Arc C is compact proof for i being Element of NAT holds (Lower_Appr C) . i c= Cl (RightComp (Cage (C,0))) by Th2; then Lim_inf (Lower_Appr C) is compact by KURATO_2:26; hence South_Arc C is compact by JORDAN19:def_4; ::_thesis: verum end; end; Lm2: dom proj2 = the carrier of (TOP-REAL 2) by FUNCT_2:def_1; Lm3: for R being non empty Subset of (TOP-REAL 2) for n being Element of NAT holds 1 <= len (Gauge (R,n)) proof let R be non empty Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT holds 1 <= len (Gauge (R,n)) let n be Element of NAT ; ::_thesis: 1 <= len (Gauge (R,n)) 4 <= len (Gauge (R,n)) by JORDAN8:10; hence 1 <= len (Gauge (R,n)) by XXREAL_0:2; ::_thesis: verum end; theorem Th5: :: JORDAN22:5 for R being non empty Subset of (TOP-REAL 2) for n being Element of NAT holds [1,1] in Indices (Gauge (R,n)) proof let R be non empty Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT holds [1,1] in Indices (Gauge (R,n)) let n be Element of NAT ; ::_thesis: [1,1] in Indices (Gauge (R,n)) A1: len (Gauge (R,n)) = width (Gauge (R,n)) by JORDAN8:def_1; 1 <= len (Gauge (R,n)) by Lm3; hence [1,1] in Indices (Gauge (R,n)) by A1, MATRIX_1:36; ::_thesis: verum end; theorem Th6: :: JORDAN22:6 for R being non empty Subset of (TOP-REAL 2) for n being Element of NAT holds [1,2] in Indices (Gauge (R,n)) proof let R be non empty Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT holds [1,2] in Indices (Gauge (R,n)) let n be Element of NAT ; ::_thesis: [1,2] in Indices (Gauge (R,n)) A1: len (Gauge (R,n)) = width (Gauge (R,n)) by JORDAN8:def_1; A2: 4 <= len (Gauge (R,n)) by JORDAN8:10; then A3: 2 <= len (Gauge (R,n)) by XXREAL_0:2; 1 <= len (Gauge (R,n)) by A2, XXREAL_0:2; hence [1,2] in Indices (Gauge (R,n)) by A1, A3, MATRIX_1:36; ::_thesis: verum end; theorem Th7: :: JORDAN22:7 for R being non empty Subset of (TOP-REAL 2) for n being Element of NAT holds [2,1] in Indices (Gauge (R,n)) proof let R be non empty Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT holds [2,1] in Indices (Gauge (R,n)) let n be Element of NAT ; ::_thesis: [2,1] in Indices (Gauge (R,n)) A1: len (Gauge (R,n)) = width (Gauge (R,n)) by JORDAN8:def_1; A2: 4 <= len (Gauge (R,n)) by JORDAN8:10; then A3: 2 <= len (Gauge (R,n)) by XXREAL_0:2; 1 <= len (Gauge (R,n)) by A2, XXREAL_0:2; hence [2,1] in Indices (Gauge (R,n)) by A1, A3, MATRIX_1:36; ::_thesis: verum end; theorem Th8: :: JORDAN22:8 for i, m, k, j being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m > k & [i,j] in Indices (Gauge (C,k)) & [i,(j + 1)] in Indices (Gauge (C,k)) holds dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * (i,(j + 1)))) < dist (((Gauge (C,k)) * (i,j)),((Gauge (C,k)) * (i,(j + 1)))) proof let i, m, k, j be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m > k & [i,j] in Indices (Gauge (C,k)) & [i,(j + 1)] in Indices (Gauge (C,k)) holds dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * (i,(j + 1)))) < dist (((Gauge (C,k)) * (i,j)),((Gauge (C,k)) * (i,(j + 1)))) let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( m > k & [i,j] in Indices (Gauge (C,k)) & [i,(j + 1)] in Indices (Gauge (C,k)) implies dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * (i,(j + 1)))) < dist (((Gauge (C,k)) * (i,j)),((Gauge (C,k)) * (i,(j + 1)))) ) assume that A1: m > k and A2: [i,j] in Indices (Gauge (C,k)) and A3: [i,(j + 1)] in Indices (Gauge (C,k)) ; ::_thesis: dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * (i,(j + 1)))) < dist (((Gauge (C,k)) * (i,j)),((Gauge (C,k)) * (i,(j + 1)))) A4: len (Gauge (C,k)) < len (Gauge (C,m)) by A1, JORDAN1A:29; A5: len (Gauge (C,m)) = width (Gauge (C,m)) by JORDAN8:def_1; A6: len (Gauge (C,k)) = width (Gauge (C,k)) by JORDAN8:def_1; j <= width (Gauge (C,k)) by A2, MATRIX_1:38; then A7: j <= width (Gauge (C,m)) by A6, A5, A4, XXREAL_0:2; A8: (N-bound C) - (S-bound C) > 0 by SPRECT_1:32, XREAL_1:50; i <= len (Gauge (C,k)) by A2, MATRIX_1:38; then A9: i <= len (Gauge (C,m)) by A4, XXREAL_0:2; j + 1 <= width (Gauge (C,k)) by A3, MATRIX_1:38; then A10: j + 1 <= width (Gauge (C,m)) by A6, A5, A4, XXREAL_0:2; A11: 1 <= i by A2, MATRIX_1:38; 1 <= j + 1 by NAT_1:11; then A12: [i,(j + 1)] in Indices (Gauge (C,m)) by A11, A9, A10, MATRIX_1:36; 1 <= j by A2, MATRIX_1:38; then [i,j] in Indices (Gauge (C,m)) by A11, A9, A7, MATRIX_1:36; then A13: dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * (i,(j + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ m) by A12, GOBRD14:9; A14: 2 |^ k > 0 by NEWTON:83; dist (((Gauge (C,k)) * (i,j)),((Gauge (C,k)) * (i,(j + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ k) by A2, A3, GOBRD14:9; hence dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * (i,(j + 1)))) < dist (((Gauge (C,k)) * (i,j)),((Gauge (C,k)) * (i,(j + 1)))) by A1, A13, A14, A8, PEPIN:66, XREAL_1:76; ::_thesis: verum end; theorem Th9: :: JORDAN22:9 for m, k being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m > k holds dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,2))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,2))) proof let m, k be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m > k holds dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,2))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,2))) let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( m > k implies dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,2))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,2))) ) assume A1: m > k ; ::_thesis: dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,2))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,2))) [1,(1 + 1)] in Indices (Gauge (C,k)) by Th6; hence dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,2))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,2))) by A1, Th5, Th8; ::_thesis: verum end; theorem Th10: :: JORDAN22:10 for i, m, k, j being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m > k & [i,j] in Indices (Gauge (C,k)) & [(i + 1),j] in Indices (Gauge (C,k)) holds dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * ((i + 1),j))) < dist (((Gauge (C,k)) * (i,j)),((Gauge (C,k)) * ((i + 1),j))) proof let i, m, k, j be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m > k & [i,j] in Indices (Gauge (C,k)) & [(i + 1),j] in Indices (Gauge (C,k)) holds dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * ((i + 1),j))) < dist (((Gauge (C,k)) * (i,j)),((Gauge (C,k)) * ((i + 1),j))) let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( m > k & [i,j] in Indices (Gauge (C,k)) & [(i + 1),j] in Indices (Gauge (C,k)) implies dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * ((i + 1),j))) < dist (((Gauge (C,k)) * (i,j)),((Gauge (C,k)) * ((i + 1),j))) ) assume that A1: m > k and A2: [i,j] in Indices (Gauge (C,k)) and A3: [(i + 1),j] in Indices (Gauge (C,k)) ; ::_thesis: dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * ((i + 1),j))) < dist (((Gauge (C,k)) * (i,j)),((Gauge (C,k)) * ((i + 1),j))) A4: len (Gauge (C,k)) < len (Gauge (C,m)) by A1, JORDAN1A:29; i <= len (Gauge (C,k)) by A2, MATRIX_1:38; then A5: i <= len (Gauge (C,m)) by A4, XXREAL_0:2; A6: (E-bound C) - (W-bound C) > 0 by SPRECT_1:31, XREAL_1:50; A7: len (Gauge (C,m)) = width (Gauge (C,m)) by JORDAN8:def_1; A8: len (Gauge (C,k)) = width (Gauge (C,k)) by JORDAN8:def_1; j <= width (Gauge (C,k)) by A2, MATRIX_1:38; then A9: j <= width (Gauge (C,m)) by A8, A7, A4, XXREAL_0:2; i + 1 <= len (Gauge (C,k)) by A3, MATRIX_1:38; then A10: i + 1 <= len (Gauge (C,m)) by A4, XXREAL_0:2; A11: 1 <= j by A2, MATRIX_1:38; 1 <= i + 1 by NAT_1:11; then A12: [(i + 1),j] in Indices (Gauge (C,m)) by A11, A9, A10, MATRIX_1:36; 1 <= i by A2, MATRIX_1:38; then [i,j] in Indices (Gauge (C,m)) by A11, A5, A9, MATRIX_1:36; then A13: dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * ((i + 1),j))) = ((E-bound C) - (W-bound C)) / (2 |^ m) by A12, GOBRD14:10; A14: 2 |^ k > 0 by NEWTON:83; dist (((Gauge (C,k)) * (i,j)),((Gauge (C,k)) * ((i + 1),j))) = ((E-bound C) - (W-bound C)) / (2 |^ k) by A2, A3, GOBRD14:10; hence dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * ((i + 1),j))) < dist (((Gauge (C,k)) * (i,j)),((Gauge (C,k)) * ((i + 1),j))) by A1, A13, A14, A6, PEPIN:66, XREAL_1:76; ::_thesis: verum end; theorem Th11: :: JORDAN22:11 for m, k being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m > k holds dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (2,1))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (2,1))) proof let m, k be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m > k holds dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (2,1))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (2,1))) let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( m > k implies dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (2,1))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (2,1))) ) assume A1: m > k ; ::_thesis: dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (2,1))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (2,1))) [(1 + 1),1] in Indices (Gauge (C,k)) by Th7; hence dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (2,1))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (2,1))) by A1, Th5, Th10; ::_thesis: verum end; theorem :: JORDAN22:12 for C being Simple_closed_curve for i being Element of NAT for r, t being real number st r > 0 & t > 0 holds ex n being Element of NAT st ( i < n & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < t ) proof let C be Simple_closed_curve; ::_thesis: for i being Element of NAT for r, t being real number st r > 0 & t > 0 holds ex n being Element of NAT st ( i < n & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < t ) let i be Element of NAT ; ::_thesis: for r, t being real number st r > 0 & t > 0 holds ex n being Element of NAT st ( i < n & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < t ) let r, t be real number ; ::_thesis: ( r > 0 & t > 0 implies ex n being Element of NAT st ( i < n & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < t ) ) assume that A1: r > 0 and A2: t > 0 ; ::_thesis: ex n being Element of NAT st ( i < n & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < t ) consider n being Element of NAT such that 1 < n and A3: dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r and A4: dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < t by A1, A2, GOBRD14:11; percases ( i < n or i >= n ) ; supposeA5: i < n ; ::_thesis: ex n being Element of NAT st ( i < n & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < t ) take n ; ::_thesis: ( i < n & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < t ) thus ( i < n & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < t ) by A3, A4, A5; ::_thesis: verum end; supposeA6: i >= n ; ::_thesis: ex n being Element of NAT st ( i < n & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < t ) take i + 1 ; ::_thesis: ( i < i + 1 & dist (((Gauge (C,(i + 1))) * (1,1)),((Gauge (C,(i + 1))) * (1,2))) < r & dist (((Gauge (C,(i + 1))) * (1,1)),((Gauge (C,(i + 1))) * (2,1))) < t ) A7: ( i > n or i = n ) by A6, XXREAL_0:1; then A8: dist (((Gauge (C,i)) * (1,1)),((Gauge (C,i)) * (2,1))) <= dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) by Th11; A9: dist (((Gauge (C,i)) * (1,1)),((Gauge (C,i)) * (1,2))) <= dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) by A7, Th9; thus A10: i < i + 1 by NAT_1:13; ::_thesis: ( dist (((Gauge (C,(i + 1))) * (1,1)),((Gauge (C,(i + 1))) * (1,2))) < r & dist (((Gauge (C,(i + 1))) * (1,1)),((Gauge (C,(i + 1))) * (2,1))) < t ) then dist (((Gauge (C,(i + 1))) * (1,1)),((Gauge (C,(i + 1))) * (1,2))) < dist (((Gauge (C,i)) * (1,1)),((Gauge (C,i)) * (1,2))) by Th9; then A11: dist (((Gauge (C,(i + 1))) * (1,1)),((Gauge (C,(i + 1))) * (1,2))) < dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) by A9, XXREAL_0:2; dist (((Gauge (C,(i + 1))) * (1,1)),((Gauge (C,(i + 1))) * (2,1))) < dist (((Gauge (C,i)) * (1,1)),((Gauge (C,i)) * (2,1))) by A10, Th11; then dist (((Gauge (C,(i + 1))) * (1,1)),((Gauge (C,(i + 1))) * (2,1))) < dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) by A8, XXREAL_0:2; hence ( dist (((Gauge (C,(i + 1))) * (1,1)),((Gauge (C,(i + 1))) * (1,2))) < r & dist (((Gauge (C,(i + 1))) * (1,1)),((Gauge (C,(i + 1))) * (2,1))) < t ) by A3, A4, A11, XXREAL_0:2; ::_thesis: verum end; end; end; theorem Th13: :: JORDAN22:13 for C being Simple_closed_curve for n being Element of NAT st 0 < n holds upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))) = upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)))) proof let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st 0 < n holds upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))) = upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)))) let n be Element of NAT ; ::_thesis: ( 0 < n implies upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))) = upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)))) ) set f = Cage (C,n); set G = Gauge (C,n); set c = Center (Gauge (C,n)); set Y = proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))); set X = proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))); A1: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; A2: 1 <= len (Gauge (C,n)) by Lm3; assume 0 < n ; ::_thesis: upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))) = upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)))) then A3: ((Gauge (C,n)) * ((Center (Gauge (C,n))),1)) `1 = ((W-bound C) + (E-bound C)) / 2 by A1, A2, JORDAN1G:35 .= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by JORDAN1G:33 ; then A4: (Gauge (C,n)) * ((Center (Gauge (C,n))),1) in Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2) ; A5: proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))) is bounded_above by JORDAN21:13; LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))) meets Upper_Arc (L~ (Cage (C,n))) by JORDAN1B:31; then LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))) meets L~ (Cage (C,n)) by JORDAN6:61, XBOOLE_1:63; then A6: not (L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))) is empty by XBOOLE_0:def_7; then A7: not proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) is empty by Lm2, RELAT_1:119; A8: Center (Gauge (C,n)) <= len (Gauge (C,n)) by JORDAN1B:13; 1 <= Center (Gauge (C,n)) by JORDAN1B:11; then A9: ((Gauge (C,n)) * ((Center (Gauge (C,n))),1)) `1 = ((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))) `1 by A1, A2, A8, GOBOARD5:2; then (Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))) in Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2) by A3; then A10: ((L~ (Cage (C,n))) /\ (L~ (Cage (C,n)))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))) c= (L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)) by A4, JORDAN1A:13, XBOOLE_1:26; then A11: proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) c= proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))) by RELAT_1:123; then A12: for r being real number st r in proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) holds r <= upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)))) by A5, SEQ_4:def_1; A13: not proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))) is empty by A11, A6, Lm2, RELAT_1:119, XBOOLE_1:3; A14: for s being real number st 0 < s holds ex r being real number st ( r in proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) & (upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) - s < r ) proof let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st ( r in proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) & (upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) - s < r ) ) assume 0 < s ; ::_thesis: ex r being real number st ( r in proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) & (upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) - s < r ) then consider r being real number such that A15: r in proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))) and A16: (upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) - s < r by A5, A13, SEQ_4:def_1; take r ; ::_thesis: ( r in proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) & (upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) - s < r ) consider x being Point of (TOP-REAL 2) such that A17: x in (L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)) and A18: proj2 . x = r by A15, Lm1; A19: x in L~ (Cage (C,n)) by A17, XBOOLE_0:def_4; x in Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2) by A17, XBOOLE_0:def_4; then A20: ((Gauge (C,n)) * ((Center (Gauge (C,n))),1)) `1 = x `1 by A3, JORDAN6:31; A21: GoB (Cage (C,n)) = Gauge (C,n) by JORDAN1H:44; then A22: ((Gauge (C,n)) * ((Center (Gauge (C,n))),1)) `2 <= x `2 by A8, A19, JORDAN1B:11, JORDAN5D:33; x `2 <= ((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))) `2 by A1, A8, A19, A21, JORDAN1B:11, JORDAN5D:34; then x in LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))) by A9, A20, A22, GOBOARD7:7; then x in (L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))) by A19, XBOOLE_0:def_4; hence r in proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) by A18, FUNCT_2:35; ::_thesis: (upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) - s < r thus (upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) - s < r by A16; ::_thesis: verum end; proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) is bounded_above by A10, A5, RELAT_1:123, XXREAL_2:43; hence upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))) = upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)))) by A7, A12, A14, SEQ_4:def_1; ::_thesis: verum end; theorem Th14: :: JORDAN22:14 for C being Simple_closed_curve for n being Element of NAT st 0 < n holds lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))) = lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)))) proof let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st 0 < n holds lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))) = lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)))) let n be Element of NAT ; ::_thesis: ( 0 < n implies lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))) = lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)))) ) set f = Cage (C,n); set G = Gauge (C,n); set c = Center (Gauge (C,n)); set Y = proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))); set X = proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))); A1: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; A2: 1 <= len (Gauge (C,n)) by Lm3; assume 0 < n ; ::_thesis: lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))) = lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)))) then A3: ((Gauge (C,n)) * ((Center (Gauge (C,n))),1)) `1 = ((W-bound C) + (E-bound C)) / 2 by A1, A2, JORDAN1G:35 .= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by JORDAN1G:33 ; then A4: (Gauge (C,n)) * ((Center (Gauge (C,n))),1) in Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2) ; A5: proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))) is bounded_below by JORDAN21:13; LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))) meets Upper_Arc (L~ (Cage (C,n))) by JORDAN1B:31; then LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))) meets L~ (Cage (C,n)) by JORDAN6:61, XBOOLE_1:63; then A6: not (L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))) is empty by XBOOLE_0:def_7; then A7: not proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) is empty by Lm2, RELAT_1:119; A8: Center (Gauge (C,n)) <= len (Gauge (C,n)) by JORDAN1B:13; 1 <= Center (Gauge (C,n)) by JORDAN1B:11; then A9: ((Gauge (C,n)) * ((Center (Gauge (C,n))),1)) `1 = ((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))) `1 by A1, A2, A8, GOBOARD5:2; then (Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))) in Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2) by A3; then A10: ((L~ (Cage (C,n))) /\ (L~ (Cage (C,n)))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))) c= (L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)) by A4, JORDAN1A:13, XBOOLE_1:26; then A11: proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) c= proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))) by RELAT_1:123; then A12: for r being real number st r in proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) holds lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)))) <= r by A5, SEQ_4:def_2; A13: not proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))) is empty by A11, A6, Lm2, RELAT_1:119, XBOOLE_1:3; A14: for s being real number st 0 < s holds ex r being real number st ( r in proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) & r < (lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) + s ) proof let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st ( r in proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) & r < (lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) + s ) ) assume 0 < s ; ::_thesis: ex r being real number st ( r in proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) & r < (lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) + s ) then consider r being real number such that A15: r in proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))) and A16: r < (lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) + s by A5, A13, SEQ_4:def_2; take r ; ::_thesis: ( r in proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) & r < (lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) + s ) consider x being Point of (TOP-REAL 2) such that A17: x in (L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)) and A18: proj2 . x = r by A15, Lm1; A19: x in L~ (Cage (C,n)) by A17, XBOOLE_0:def_4; x in Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2) by A17, XBOOLE_0:def_4; then A20: ((Gauge (C,n)) * ((Center (Gauge (C,n))),1)) `1 = x `1 by A3, JORDAN6:31; A21: GoB (Cage (C,n)) = Gauge (C,n) by JORDAN1H:44; then A22: ((Gauge (C,n)) * ((Center (Gauge (C,n))),1)) `2 <= x `2 by A8, A19, JORDAN1B:11, JORDAN5D:33; x `2 <= ((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))) `2 by A1, A8, A19, A21, JORDAN1B:11, JORDAN5D:34; then x in LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))) by A9, A20, A22, GOBOARD7:7; then x in (L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))) by A19, XBOOLE_0:def_4; hence r in proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) by A18, FUNCT_2:35; ::_thesis: r < (lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) + s thus r < (lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) + s by A16; ::_thesis: verum end; proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) is bounded_below by A10, A5, RELAT_1:123, XXREAL_2:44; hence lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))) = lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)))) by A7, A12, A14, SEQ_4:def_2; ::_thesis: verum end; theorem :: JORDAN22:15 for C being Simple_closed_curve for n being Element of NAT st 0 < n holds UMP (L~ (Cage (C,n))) = |[(((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2),(upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))))]| by Th13; theorem :: JORDAN22:16 for C being Simple_closed_curve for n being Element of NAT st 0 < n holds LMP (L~ (Cage (C,n))) = |[(((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2),(lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))))]| by Th14; theorem Th17: :: JORDAN22:17 for C being Simple_closed_curve for n being Element of NAT holds (UMP C) `2 < (UMP (L~ (Cage (C,n)))) `2 proof let C be Simple_closed_curve; ::_thesis: for n being Element of NAT holds (UMP C) `2 < (UMP (L~ (Cage (C,n)))) `2 let n be Element of NAT ; ::_thesis: (UMP C) `2 < (UMP (L~ (Cage (C,n)))) `2 set p = UMP (L~ (Cage (C,n))); set u = UMP C; set w = ((W-bound C) + (E-bound C)) / 2; A1: (UMP C) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52; A2: UMP (L~ (Cage (C,n))) in L~ (Cage (C,n)) by JORDAN21:30; A3: UMP C = |[((UMP C) `1),((UMP C) `2)]| by EUCLID:53; A4: UMP (L~ (Cage (C,n))) = |[((UMP (L~ (Cage (C,n)))) `1),((UMP (L~ (Cage (C,n)))) `2)]| by EUCLID:53; A5: C misses L~ (Cage (C,n)) by JORDAN10:5; A6: UMP C in C by JORDAN21:30; A7: ((W-bound C) + (E-bound C)) / 2 = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by JORDAN1G:33; then A8: (UMP (L~ (Cage (C,n)))) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52; assume A9: not (UMP C) `2 < (UMP (L~ (Cage (C,n)))) `2 ; ::_thesis: contradiction percases ( (UMP C) `2 = (UMP (L~ (Cage (C,n)))) `2 or (UMP C) `2 > (UMP (L~ (Cage (C,n)))) `2 ) by A9, XXREAL_0:1; suppose (UMP C) `2 = (UMP (L~ (Cage (C,n)))) `2 ; ::_thesis: contradiction hence contradiction by A1, A8, A4, A3, A5, A6, A2, XBOOLE_0:3; ::_thesis: verum end; supposeA10: (UMP C) `2 > (UMP (L~ (Cage (C,n)))) `2 ; ::_thesis: contradiction A11: ( not proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is empty & proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is bounded_above ) by A7, JORDAN21:12, JORDAN21:13; A12: (UMP (L~ (Cage (C,n)))) `2 = upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)))) by A7, EUCLID:52; A13: (north_halfline (UMP (L~ (Cage (C,n))))) \ {(UMP (L~ (Cage (C,n))))} misses L~ (Cage (C,n)) proof assume (north_halfline (UMP (L~ (Cage (C,n))))) \ {(UMP (L~ (Cage (C,n))))} meets L~ (Cage (C,n)) ; ::_thesis: contradiction then consider x being set such that A14: x in (north_halfline (UMP (L~ (Cage (C,n))))) \ {(UMP (L~ (Cage (C,n))))} and A15: x in L~ (Cage (C,n)) by XBOOLE_0:3; reconsider x = x as Point of (TOP-REAL 2) by A15; A16: x in north_halfline (UMP (L~ (Cage (C,n)))) by A14, XBOOLE_0:def_5; then A17: x `2 >= (UMP (L~ (Cage (C,n)))) `2 by TOPREAL1:def_10; A18: x `1 = ((W-bound C) + (E-bound C)) / 2 by A8, A16, TOPREAL1:def_10; then x in Vertical_Line (((W-bound C) + (E-bound C)) / 2) ; then A19: x in (L~ (Cage (C,n))) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) by A15, XBOOLE_0:def_4; proj2 . x = x `2 by PSCOMP_1:def_6; then x `2 in proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) by A19, FUNCT_2:35; then A20: x `2 <= (UMP (L~ (Cage (C,n)))) `2 by A12, A11, SEQ_4:def_1; not x in {(UMP (L~ (Cage (C,n))))} by A14, XBOOLE_0:def_5; then x <> UMP (L~ (Cage (C,n))) by TARSKI:def_1; then x `2 <> (UMP (L~ (Cage (C,n)))) `2 by A8, A18, TOPREAL3:6; hence contradiction by A17, A20, XXREAL_0:1; ::_thesis: verum end; (north_halfline (UMP (L~ (Cage (C,n))))) \ {(UMP (L~ (Cage (C,n))))} is convex by JORDAN21:6; then A21: ( (north_halfline (UMP (L~ (Cage (C,n))))) \ {(UMP (L~ (Cage (C,n))))} c= UBD (L~ (Cage (C,n))) or (north_halfline (UMP (L~ (Cage (C,n))))) \ {(UMP (L~ (Cage (C,n))))} c= BDD (L~ (Cage (C,n))) ) by A13, JORDAN1K:19; A22: UBD (L~ (Cage (C,n))) c= UBD C by JORDAN10:13; A23: not UMP C in {(UMP (L~ (Cage (C,n))))} by A10, TARSKI:def_1; UMP C in north_halfline (UMP (L~ (Cage (C,n)))) by A1, A8, A10, TOPREAL1:def_10; then A24: UMP C in (north_halfline (UMP (L~ (Cage (C,n))))) \ {(UMP (L~ (Cage (C,n))))} by A23, XBOOLE_0:def_5; A25: UBD C misses C by JORDAN21:10; not north_halfline (UMP (L~ (Cage (C,n)))) is bounded by JORDAN2C:122; then A26: not (north_halfline (UMP (L~ (Cage (C,n))))) \ {(UMP (L~ (Cage (C,n))))} is bounded by JORDAN21:1, TOPREAL6:90; BDD (L~ (Cage (C,n))) is bounded by JORDAN2C:106; then UMP C in UBD (L~ (Cage (C,n))) by A21, A26, A24, RLTOPSP1:42; hence contradiction by A6, A22, A25, XBOOLE_0:3; ::_thesis: verum end; end; end; theorem Th18: :: JORDAN22:18 for C being Simple_closed_curve for n being Element of NAT holds (LMP C) `2 > (LMP (L~ (Cage (C,n)))) `2 proof let C be Simple_closed_curve; ::_thesis: for n being Element of NAT holds (LMP C) `2 > (LMP (L~ (Cage (C,n)))) `2 let n be Element of NAT ; ::_thesis: (LMP C) `2 > (LMP (L~ (Cage (C,n)))) `2 set p = LMP (L~ (Cage (C,n))); set u = LMP C; set w = ((W-bound C) + (E-bound C)) / 2; A1: (LMP C) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52; A2: LMP (L~ (Cage (C,n))) in L~ (Cage (C,n)) by JORDAN21:31; A3: LMP C = |[((LMP C) `1),((LMP C) `2)]| by EUCLID:53; A4: LMP (L~ (Cage (C,n))) = |[((LMP (L~ (Cage (C,n)))) `1),((LMP (L~ (Cage (C,n)))) `2)]| by EUCLID:53; A5: C misses L~ (Cage (C,n)) by JORDAN10:5; A6: LMP C in C by JORDAN21:31; A7: ((W-bound C) + (E-bound C)) / 2 = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2 by JORDAN1G:33; then A8: (LMP (L~ (Cage (C,n)))) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52; assume A9: not (LMP C) `2 > (LMP (L~ (Cage (C,n)))) `2 ; ::_thesis: contradiction percases ( (LMP C) `2 = (LMP (L~ (Cage (C,n)))) `2 or (LMP C) `2 < (LMP (L~ (Cage (C,n)))) `2 ) by A9, XXREAL_0:1; suppose (LMP C) `2 = (LMP (L~ (Cage (C,n)))) `2 ; ::_thesis: contradiction hence contradiction by A1, A8, A4, A3, A5, A6, A2, XBOOLE_0:3; ::_thesis: verum end; supposeA10: (LMP C) `2 < (LMP (L~ (Cage (C,n)))) `2 ; ::_thesis: contradiction A11: ( not proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is empty & proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is bounded_below ) by A7, JORDAN21:12, JORDAN21:13; A12: (LMP (L~ (Cage (C,n)))) `2 = lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)))) by A7, EUCLID:52; A13: (south_halfline (LMP (L~ (Cage (C,n))))) \ {(LMP (L~ (Cage (C,n))))} misses L~ (Cage (C,n)) proof assume (south_halfline (LMP (L~ (Cage (C,n))))) \ {(LMP (L~ (Cage (C,n))))} meets L~ (Cage (C,n)) ; ::_thesis: contradiction then consider x being set such that A14: x in (south_halfline (LMP (L~ (Cage (C,n))))) \ {(LMP (L~ (Cage (C,n))))} and A15: x in L~ (Cage (C,n)) by XBOOLE_0:3; reconsider x = x as Point of (TOP-REAL 2) by A15; A16: x in south_halfline (LMP (L~ (Cage (C,n)))) by A14, XBOOLE_0:def_5; then A17: x `2 <= (LMP (L~ (Cage (C,n)))) `2 by TOPREAL1:def_12; A18: x `1 = ((W-bound C) + (E-bound C)) / 2 by A8, A16, TOPREAL1:def_12; then x in Vertical_Line (((W-bound C) + (E-bound C)) / 2) ; then A19: x in (L~ (Cage (C,n))) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) by A15, XBOOLE_0:def_4; proj2 . x = x `2 by PSCOMP_1:def_6; then x `2 in proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) by A19, FUNCT_2:35; then A20: x `2 >= (LMP (L~ (Cage (C,n)))) `2 by A12, A11, SEQ_4:def_2; not x in {(LMP (L~ (Cage (C,n))))} by A14, XBOOLE_0:def_5; then x <> LMP (L~ (Cage (C,n))) by TARSKI:def_1; then x `2 <> (LMP (L~ (Cage (C,n)))) `2 by A8, A18, TOPREAL3:6; hence contradiction by A17, A20, XXREAL_0:1; ::_thesis: verum end; (south_halfline (LMP (L~ (Cage (C,n))))) \ {(LMP (L~ (Cage (C,n))))} is convex by JORDAN21:7; then A21: ( (south_halfline (LMP (L~ (Cage (C,n))))) \ {(LMP (L~ (Cage (C,n))))} c= UBD (L~ (Cage (C,n))) or (south_halfline (LMP (L~ (Cage (C,n))))) \ {(LMP (L~ (Cage (C,n))))} c= BDD (L~ (Cage (C,n))) ) by A13, JORDAN1K:19; A22: UBD (L~ (Cage (C,n))) c= UBD C by JORDAN10:13; A23: not LMP C in {(LMP (L~ (Cage (C,n))))} by A10, TARSKI:def_1; LMP C in south_halfline (LMP (L~ (Cage (C,n)))) by A1, A8, A10, TOPREAL1:def_12; then A24: LMP C in (south_halfline (LMP (L~ (Cage (C,n))))) \ {(LMP (L~ (Cage (C,n))))} by A23, XBOOLE_0:def_5; A25: UBD C misses C by JORDAN21:10; not south_halfline (LMP (L~ (Cage (C,n)))) is bounded by JORDAN2C:123; then A26: not (south_halfline (LMP (L~ (Cage (C,n))))) \ {(LMP (L~ (Cage (C,n))))} is bounded by JORDAN21:1, TOPREAL6:90; BDD (L~ (Cage (C,n))) is bounded by JORDAN2C:106; then LMP C in UBD (L~ (Cage (C,n))) by A21, A26, A24, RLTOPSP1:42; hence contradiction by A6, A22, A25, XBOOLE_0:3; ::_thesis: verum end; end; end; theorem Th19: :: JORDAN22:19 for C being Simple_closed_curve for n being Element of NAT st 0 < n holds ex i being Element of NAT st ( 1 <= i & i <= len (Gauge (C,n)) & UMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) ) proof let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st 0 < n holds ex i being Element of NAT st ( 1 <= i & i <= len (Gauge (C,n)) & UMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) ) let n be Element of NAT ; ::_thesis: ( 0 < n implies ex i being Element of NAT st ( 1 <= i & i <= len (Gauge (C,n)) & UMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) ) ) set f = Cage (C,n); set G = Gauge (C,n); set w = Center (Gauge (C,n)); A1: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; A2: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))) meets Upper_Arc (L~ (Cage (C,n))) by JORDAN1B:31; then A3: LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))) meets L~ (Cage (C,n)) by JORDAN6:61, XBOOLE_1:63; A4: Center (Gauge (C,n)) <= len (Gauge (C,n)) by JORDAN1B:13; assume A5: 0 < n ; ::_thesis: ex i being Element of NAT st ( 1 <= i & i <= len (Gauge (C,n)) & UMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) ) then UMP (L~ (Cage (C,n))) = |[(((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2),(upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))))]| by Th13; then A6: (UMP (L~ (Cage (C,n)))) `2 = upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))) by EUCLID:52; A7: 1 <= len (Gauge (C,n)) by Lm3; A8: 1 <= Center (Gauge (C,n)) by JORDAN1B:11; then A9: [(Center (Gauge (C,n))),(len (Gauge (C,n)))] in Indices (Gauge (C,n)) by A2, A7, A4, MATRIX_1:36; [(Center (Gauge (C,n))),1] in Indices (Gauge (C,n)) by A2, A7, A8, A4, MATRIX_1:36; then consider i being Element of NAT such that A10: 1 <= i and A11: i <= len (Gauge (C,n)) and A12: ((Gauge (C,n)) * ((Center (Gauge (C,n))),i)) `2 = upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))) /\ (L~ (Cage (C,n))))) by A1, A3, A7, A9, JORDAN1F:2; A13: (UMP (L~ (Cage (C,n)))) `1 = ((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2 by EUCLID:52; take i ; ::_thesis: ( 1 <= i & i <= len (Gauge (C,n)) & UMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) ) thus ( 1 <= i & i <= len (Gauge (C,n)) ) by A10, A11; ::_thesis: UMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) ((Gauge (C,n)) * ((Center (Gauge (C,n))),i)) `1 = ((W-bound C) + (E-bound C)) / 2 by A5, A2, A10, A11, JORDAN1G:35; then (UMP (L~ (Cage (C,n)))) `1 = ((Gauge (C,n)) * ((Center (Gauge (C,n))),i)) `1 by A13, JORDAN1G:33; hence UMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) by A12, A6, TOPREAL3:6; ::_thesis: verum end; theorem Th20: :: JORDAN22:20 for C being Simple_closed_curve for n being Element of NAT st 0 < n holds ex i being Element of NAT st ( 1 <= i & i <= len (Gauge (C,n)) & LMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) ) proof let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st 0 < n holds ex i being Element of NAT st ( 1 <= i & i <= len (Gauge (C,n)) & LMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) ) let n be Element of NAT ; ::_thesis: ( 0 < n implies ex i being Element of NAT st ( 1 <= i & i <= len (Gauge (C,n)) & LMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) ) ) set f = Cage (C,n); set G = Gauge (C,n); set w = Center (Gauge (C,n)); A1: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; A2: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))) meets Upper_Arc (L~ (Cage (C,n))) by JORDAN1B:31; then A3: LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))) meets L~ (Cage (C,n)) by JORDAN6:61, XBOOLE_1:63; A4: Center (Gauge (C,n)) <= len (Gauge (C,n)) by JORDAN1B:13; assume A5: 0 < n ; ::_thesis: ex i being Element of NAT st ( 1 <= i & i <= len (Gauge (C,n)) & LMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) ) then LMP (L~ (Cage (C,n))) = |[(((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2),(lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))))]| by Th14; then A6: (LMP (L~ (Cage (C,n)))) `2 = lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))) by EUCLID:52; A7: 1 <= len (Gauge (C,n)) by Lm3; A8: 1 <= Center (Gauge (C,n)) by JORDAN1B:11; then A9: [(Center (Gauge (C,n))),(len (Gauge (C,n)))] in Indices (Gauge (C,n)) by A2, A7, A4, MATRIX_1:36; [(Center (Gauge (C,n))),1] in Indices (Gauge (C,n)) by A2, A7, A8, A4, MATRIX_1:36; then consider i being Element of NAT such that A10: 1 <= i and A11: i <= len (Gauge (C,n)) and A12: ((Gauge (C,n)) * ((Center (Gauge (C,n))),i)) `2 = lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))) /\ (L~ (Cage (C,n))))) by A1, A3, A7, A9, JORDAN1F:1; A13: (LMP (L~ (Cage (C,n)))) `1 = ((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2 by EUCLID:52; take i ; ::_thesis: ( 1 <= i & i <= len (Gauge (C,n)) & LMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) ) thus ( 1 <= i & i <= len (Gauge (C,n)) ) by A10, A11; ::_thesis: LMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) ((Gauge (C,n)) * ((Center (Gauge (C,n))),i)) `1 = ((W-bound C) + (E-bound C)) / 2 by A5, A2, A10, A11, JORDAN1G:35; then (LMP (L~ (Cage (C,n)))) `1 = ((Gauge (C,n)) * ((Center (Gauge (C,n))),i)) `1 by A13, JORDAN1G:33; hence LMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) by A12, A6, TOPREAL3:6; ::_thesis: verum end; theorem Th21: :: JORDAN22:21 for C being Simple_closed_curve for n being Element of NAT st 0 < n holds UMP (L~ (Cage (C,n))) = UMP (Upper_Arc (L~ (Cage (C,n)))) proof let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st 0 < n holds UMP (L~ (Cage (C,n))) = UMP (Upper_Arc (L~ (Cage (C,n)))) let n be Element of NAT ; ::_thesis: ( 0 < n implies UMP (L~ (Cage (C,n))) = UMP (Upper_Arc (L~ (Cage (C,n)))) ) set f = Cage (C,n); set w = ((E-bound C) + (W-bound C)) / 2; A1: Upper_Arc (L~ (Cage (C,n))) c= L~ (Cage (C,n)) by JORDAN6:61; A2: (W-bound C) + (E-bound C) = (W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n)))) by JORDAN1G:33; A3: E-bound (L~ (Cage (C,n))) = E-bound (Upper_Arc (L~ (Cage (C,n)))) by JORDAN21:18; A4: W-bound (L~ (Cage (C,n))) = W-bound (Upper_Arc (L~ (Cage (C,n)))) by JORDAN21:17; assume A5: 0 < n ; ::_thesis: UMP (L~ (Cage (C,n))) = UMP (Upper_Arc (L~ (Cage (C,n)))) then A6: 0 + 1 <= n by NAT_1:13; then A7: (n -' 1) + 1 = n by XREAL_1:235; A8: now__::_thesis:_UMP_(L~_(Cage_(C,n)))_in_Upper_Arc_(L~_(Cage_(C,n))) A9: Center (Gauge (C,1)) <= len (Gauge (C,1)) by JORDAN1B:13; A10: Center (Gauge (C,n)) <= len (Gauge (C,n)) by JORDAN1B:13; A11: (Upper_Arc (L~ (Cage (C,n)))) \/ (Lower_Arc (L~ (Cage (C,n)))) = L~ (Cage (C,n)) by JORDAN6:def_9; assume A12: not UMP (L~ (Cage (C,n))) in Upper_Arc (L~ (Cage (C,n))) ; ::_thesis: contradiction UMP (L~ (Cage (C,n))) in L~ (Cage (C,n)) by JORDAN21:30; then A13: UMP (L~ (Cage (C,n))) in Lower_Arc (L~ (Cage (C,n))) by A12, A11, XBOOLE_0:def_3; A14: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; A15: 1 <= Center (Gauge (C,n)) by JORDAN1B:11; consider j being Element of NAT such that A16: 1 <= j and A17: j <= len (Gauge (C,n)) and A18: UMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),j) by A5, Th19; set a = (Gauge (C,1)) * ((Center (Gauge (C,1))),(len (Gauge (C,1)))); set b = (Gauge (C,n)) * ((Center (Gauge (C,n))),j); set L = LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),(len (Gauge (C,1))))),((Gauge (C,n)) * ((Center (Gauge (C,n))),j))); len (Gauge (C,1)) = width (Gauge (C,1)) by JORDAN8:def_1; then LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),(len (Gauge (C,1))))),((Gauge (C,n)) * ((Center (Gauge (C,n))),j))) meets Upper_Arc (L~ (Cage (C,n))) by A7, A13, A16, A17, A18, A14, JORDAN19:5; then consider x being set such that A19: x in LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),(len (Gauge (C,1))))),((Gauge (C,n)) * ((Center (Gauge (C,n))),j))) and A20: x in Upper_Arc (L~ (Cage (C,n))) by XBOOLE_0:3; reconsider x = x as Point of (TOP-REAL 2) by A19; A21: (Gauge (C,1)) * ((Center (Gauge (C,1))),(len (Gauge (C,1)))) in LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),(len (Gauge (C,1))))),((Gauge (C,n)) * ((Center (Gauge (C,n))),j))) by RLTOPSP1:68; A22: 1 <= len (Gauge (C,1)) by Lm3; then A23: ((Gauge (C,1)) * ((Center (Gauge (C,1))),(len (Gauge (C,1))))) `1 = ((E-bound C) + (W-bound C)) / 2 by JORDAN1A:38; then A24: ((Gauge (C,n)) * ((Center (Gauge (C,n))),j)) `1 = ((E-bound C) + (W-bound C)) / 2 by A5, A16, A17, A22, JORDAN1A:36; then LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),(len (Gauge (C,1))))),((Gauge (C,n)) * ((Center (Gauge (C,n))),j))) is vertical by A23, SPPOL_1:16; then A25: x `1 = ((E-bound C) + (W-bound C)) / 2 by A19, A23, A21, SPPOL_1:def_3; then x in Vertical_Line (((E-bound C) + (W-bound C)) / 2) ; then A26: x in (Upper_Arc (L~ (Cage (C,n)))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) by A20, XBOOLE_0:def_4; then A27: (UMP (Upper_Arc (L~ (Cage (C,n))))) `2 >= x `2 by A2, A4, A3, JORDAN21:28; 1 <= Center (Gauge (C,1)) by JORDAN1B:11; then A28: ((Gauge (C,1)) * ((Center (Gauge (C,1))),(len (Gauge (C,1))))) `2 >= ((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))) `2 by A6, A15, A10, A9, JORDAN1A:40; len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; then ((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))) `2 >= ((Gauge (C,n)) * ((Center (Gauge (C,n))),j)) `2 by A16, A17, A15, A10, SPRECT_3:12; then ((Gauge (C,1)) * ((Center (Gauge (C,1))),(len (Gauge (C,1))))) `2 >= ((Gauge (C,n)) * ((Center (Gauge (C,n))),j)) `2 by A28, XXREAL_0:2; then A29: x `2 >= ((Gauge (C,n)) * ((Center (Gauge (C,n))),j)) `2 by A19, TOPREAL1:4; (UMP (L~ (Cage (C,n)))) `2 >= (UMP (Upper_Arc (L~ (Cage (C,n))))) `2 by A1, A2, A4, A3, A26, JORDAN21:13, JORDAN21:43; then ((Gauge (C,n)) * ((Center (Gauge (C,n))),j)) `2 >= x `2 by A18, A27, XXREAL_0:2; then ((Gauge (C,n)) * ((Center (Gauge (C,n))),j)) `2 = x `2 by A29, XXREAL_0:1; hence contradiction by A12, A18, A20, A24, A25, TOPREAL3:6; ::_thesis: verum end; proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is bounded_above by A2, JORDAN21:13; hence UMP (L~ (Cage (C,n))) = UMP (Upper_Arc (L~ (Cage (C,n)))) by A1, A2, A4, A3, A8, JORDAN21:21, JORDAN21:45; ::_thesis: verum end; theorem Th22: :: JORDAN22:22 for C being Simple_closed_curve for n being Element of NAT st 0 < n holds LMP (L~ (Cage (C,n))) = LMP (Lower_Arc (L~ (Cage (C,n)))) proof let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st 0 < n holds LMP (L~ (Cage (C,n))) = LMP (Lower_Arc (L~ (Cage (C,n)))) let n be Element of NAT ; ::_thesis: ( 0 < n implies LMP (L~ (Cage (C,n))) = LMP (Lower_Arc (L~ (Cage (C,n)))) ) set f = Cage (C,n); set w = ((E-bound C) + (W-bound C)) / 2; A1: Lower_Arc (L~ (Cage (C,n))) c= L~ (Cage (C,n)) by JORDAN6:61; A2: (W-bound C) + (E-bound C) = (W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n)))) by JORDAN1G:33; A3: E-bound (L~ (Cage (C,n))) = E-bound (Lower_Arc (L~ (Cage (C,n)))) by JORDAN21:20; A4: W-bound (L~ (Cage (C,n))) = W-bound (Lower_Arc (L~ (Cage (C,n)))) by JORDAN21:19; assume A5: 0 < n ; ::_thesis: LMP (L~ (Cage (C,n))) = LMP (Lower_Arc (L~ (Cage (C,n)))) then A6: 0 + 1 <= n by NAT_1:13; then A7: (n -' 1) + 1 = n by XREAL_1:235; A8: now__::_thesis:_LMP_(L~_(Cage_(C,n)))_in_Lower_Arc_(L~_(Cage_(C,n))) A9: Center (Gauge (C,1)) <= len (Gauge (C,1)) by JORDAN1B:13; A10: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; A11: (Upper_Arc (L~ (Cage (C,n)))) \/ (Lower_Arc (L~ (Cage (C,n)))) = L~ (Cage (C,n)) by JORDAN6:def_9; assume A12: not LMP (L~ (Cage (C,n))) in Lower_Arc (L~ (Cage (C,n))) ; ::_thesis: contradiction consider j being Element of NAT such that A13: 1 <= j and A14: j <= len (Gauge (C,n)) and A15: LMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),j) by A5, Th20; set a = (Gauge (C,1)) * ((Center (Gauge (C,1))),1); set b = (Gauge (C,n)) * ((Center (Gauge (C,n))),j); set L = LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),j))); A16: (Gauge (C,1)) * ((Center (Gauge (C,1))),1) in LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),j))) by RLTOPSP1:68; LMP (L~ (Cage (C,n))) in L~ (Cage (C,n)) by JORDAN21:31; then LMP (L~ (Cage (C,n))) in Upper_Arc (L~ (Cage (C,n))) by A12, A11, XBOOLE_0:def_3; then LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),j))) meets Lower_Arc (L~ (Cage (C,n))) by A7, A13, A14, A15, A10, JORDAN1J:62; then consider x being set such that A17: x in LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),j))) and A18: x in Lower_Arc (L~ (Cage (C,n))) by XBOOLE_0:3; reconsider x = x as Point of (TOP-REAL 2) by A17; A19: 1 <= Center (Gauge (C,n)) by JORDAN1B:11; A20: 1 <= len (Gauge (C,1)) by Lm3; then A21: ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `1 = ((E-bound C) + (W-bound C)) / 2 by JORDAN1A:38; then A22: ((Gauge (C,n)) * ((Center (Gauge (C,n))),j)) `1 = ((E-bound C) + (W-bound C)) / 2 by A5, A13, A14, A20, JORDAN1A:36; then LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),j))) is vertical by A21, SPPOL_1:16; then A23: x `1 = ((E-bound C) + (W-bound C)) / 2 by A17, A21, A16, SPPOL_1:def_3; then x in Vertical_Line (((E-bound C) + (W-bound C)) / 2) ; then A24: x in (Lower_Arc (L~ (Cage (C,n)))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) by A18, XBOOLE_0:def_4; then A25: (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 <= x `2 by A2, A4, A3, JORDAN21:29; A26: Center (Gauge (C,n)) <= len (Gauge (C,n)) by JORDAN1B:13; 1 <= Center (Gauge (C,1)) by JORDAN1B:11; then A27: ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `2 <= ((Gauge (C,n)) * ((Center (Gauge (C,n))),1)) `2 by A6, A19, A26, A9, JORDAN1A:43; ((Gauge (C,n)) * ((Center (Gauge (C,n))),1)) `2 <= ((Gauge (C,n)) * ((Center (Gauge (C,n))),j)) `2 by A13, A14, A10, A19, A26, SPRECT_3:12; then ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `2 <= ((Gauge (C,n)) * ((Center (Gauge (C,n))),j)) `2 by A27, XXREAL_0:2; then A28: x `2 <= ((Gauge (C,n)) * ((Center (Gauge (C,n))),j)) `2 by A17, TOPREAL1:4; (LMP (L~ (Cage (C,n)))) `2 <= (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 by A1, A2, A4, A3, A24, JORDAN21:13, JORDAN21:44; then ((Gauge (C,n)) * ((Center (Gauge (C,n))),j)) `2 <= x `2 by A15, A25, XXREAL_0:2; then ((Gauge (C,n)) * ((Center (Gauge (C,n))),j)) `2 = x `2 by A28, XXREAL_0:1; hence contradiction by A12, A15, A18, A22, A23, TOPREAL3:6; ::_thesis: verum end; proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is bounded_below by A2, JORDAN21:13; hence LMP (L~ (Cage (C,n))) = LMP (Lower_Arc (L~ (Cage (C,n)))) by A1, A2, A4, A3, A8, JORDAN21:22, JORDAN21:46; ::_thesis: verum end; theorem Th23: :: JORDAN22:23 for C being Simple_closed_curve for n being Element of NAT st 0 < n holds (UMP C) `2 < (UMP (Upper_Arc (L~ (Cage (C,n))))) `2 proof let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st 0 < n holds (UMP C) `2 < (UMP (Upper_Arc (L~ (Cage (C,n))))) `2 let n be Element of NAT ; ::_thesis: ( 0 < n implies (UMP C) `2 < (UMP (Upper_Arc (L~ (Cage (C,n))))) `2 ) assume 0 < n ; ::_thesis: (UMP C) `2 < (UMP (Upper_Arc (L~ (Cage (C,n))))) `2 then UMP (Upper_Arc (L~ (Cage (C,n)))) = UMP (L~ (Cage (C,n))) by Th21; hence (UMP C) `2 < (UMP (Upper_Arc (L~ (Cage (C,n))))) `2 by Th17; ::_thesis: verum end; theorem Th24: :: JORDAN22:24 for C being Simple_closed_curve for n being Element of NAT st 0 < n holds (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 < (LMP C) `2 proof let C be Simple_closed_curve; ::_thesis: for n being Element of NAT st 0 < n holds (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 < (LMP C) `2 let n be Element of NAT ; ::_thesis: ( 0 < n implies (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 < (LMP C) `2 ) assume 0 < n ; ::_thesis: (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 < (LMP C) `2 then LMP (Lower_Arc (L~ (Cage (C,n)))) = LMP (L~ (Cage (C,n))) by Th22; hence (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 < (LMP C) `2 by Th18; ::_thesis: verum end; theorem Th25: :: JORDAN22:25 for C being Simple_closed_curve for i, j being Element of NAT st i <= j holds (UMP (L~ (Cage (C,j)))) `2 <= (UMP (L~ (Cage (C,i)))) `2 proof let C be Simple_closed_curve; ::_thesis: for i, j being Element of NAT st i <= j holds (UMP (L~ (Cage (C,j)))) `2 <= (UMP (L~ (Cage (C,i)))) `2 let i, j be Element of NAT ; ::_thesis: ( i <= j implies (UMP (L~ (Cage (C,j)))) `2 <= (UMP (L~ (Cage (C,i)))) `2 ) set w = ((E-bound C) + (W-bound C)) / 2; set ui = UMP (L~ (Cage (C,i))); set uj = UMP (L~ (Cage (C,j))); assume i <= j ; ::_thesis: (UMP (L~ (Cage (C,j)))) `2 <= (UMP (L~ (Cage (C,i)))) `2 then A1: LeftComp (Cage (C,i)) c= LeftComp (Cage (C,j)) by JORDAN1H:47; A2: (W-bound (L~ (Cage (C,j)))) + (E-bound (L~ (Cage (C,j)))) = (W-bound C) + (E-bound C) by JORDAN1G:33; then A3: (UMP (L~ (Cage (C,j)))) `2 = upper_bound (proj2 .: ((L~ (Cage (C,j))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) by EUCLID:52; assume (UMP (L~ (Cage (C,j)))) `2 > (UMP (L~ (Cage (C,i)))) `2 ; ::_thesis: contradiction then A4: ((UMP (L~ (Cage (C,j)))) `2) - ((UMP (L~ (Cage (C,i)))) `2) > 0 by XREAL_1:50; A5: (W-bound (L~ (Cage (C,i)))) + (E-bound (L~ (Cage (C,i)))) = (W-bound C) + (E-bound C) by JORDAN1G:33; then A6: (UMP (L~ (Cage (C,i)))) `2 = upper_bound (proj2 .: ((L~ (Cage (C,i))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) by EUCLID:52; A7: ( not proj2 .: ((L~ (Cage (C,i))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is empty & proj2 .: ((L~ (Cage (C,i))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is bounded_above ) by A5, JORDAN21:12, JORDAN21:13; ( not proj2 .: ((L~ (Cage (C,j))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is empty & proj2 .: ((L~ (Cage (C,j))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is bounded_above ) by A2, JORDAN21:12, JORDAN21:13; then consider r being real number such that A8: r in proj2 .: ((L~ (Cage (C,j))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) and A9: (upper_bound (proj2 .: ((L~ (Cage (C,j))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))))) - (((UMP (L~ (Cage (C,j)))) `2) - ((UMP (L~ (Cage (C,i)))) `2)) < r by A4, SEQ_4:def_1; consider x being Point of (TOP-REAL 2) such that A10: x in (L~ (Cage (C,j))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) and A11: proj2 . x = r by A8, Lm1; A12: x `2 = r by A11, PSCOMP_1:def_6; north_halfline x misses L~ (Cage (C,i)) proof A13: x in Vertical_Line (((E-bound C) + (W-bound C)) / 2) by A10, XBOOLE_0:def_4; assume north_halfline x meets L~ (Cage (C,i)) ; ::_thesis: contradiction then consider y being set such that A14: y in north_halfline x and A15: y in L~ (Cage (C,i)) by XBOOLE_0:3; reconsider y = y as Point of (TOP-REAL 2) by A15; y `1 = x `1 by A14, TOPREAL1:def_10 .= ((E-bound C) + (W-bound C)) / 2 by A13, JORDAN6:31 ; then y in Vertical_Line (((E-bound C) + (W-bound C)) / 2) ; then A16: y in (L~ (Cage (C,i))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) by A15, XBOOLE_0:def_4; proj2 . y = y `2 by PSCOMP_1:def_6; then y `2 in proj2 .: ((L~ (Cage (C,i))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) by A16, FUNCT_2:35; then A17: y `2 <= (UMP (L~ (Cage (C,i)))) `2 by A6, A7, SEQ_4:def_1; y `2 >= x `2 by A14, TOPREAL1:def_10; hence contradiction by A3, A9, A12, A17, XXREAL_0:2; ::_thesis: verum end; then A18: north_halfline x c= UBD (L~ (Cage (C,i))) by JORDAN2C:129; x in north_halfline x by TOPREAL1:38; then x in UBD (L~ (Cage (C,i))) by A18; then A19: x in LeftComp (Cage (C,i)) by GOBRD14:36; x in L~ (Cage (C,j)) by A10, XBOOLE_0:def_4; then LeftComp (Cage (C,j)) meets L~ (Cage (C,j)) by A1, A19, XBOOLE_0:3; hence contradiction by SPRECT_3:26; ::_thesis: verum end; theorem Th26: :: JORDAN22:26 for C being Simple_closed_curve for i, j being Element of NAT st i <= j holds (LMP (L~ (Cage (C,i)))) `2 <= (LMP (L~ (Cage (C,j)))) `2 proof let C be Simple_closed_curve; ::_thesis: for i, j being Element of NAT st i <= j holds (LMP (L~ (Cage (C,i)))) `2 <= (LMP (L~ (Cage (C,j)))) `2 let i, j be Element of NAT ; ::_thesis: ( i <= j implies (LMP (L~ (Cage (C,i)))) `2 <= (LMP (L~ (Cage (C,j)))) `2 ) set w = ((E-bound C) + (W-bound C)) / 2; set ui = LMP (L~ (Cage (C,i))); set uj = LMP (L~ (Cage (C,j))); assume i <= j ; ::_thesis: (LMP (L~ (Cage (C,i)))) `2 <= (LMP (L~ (Cage (C,j)))) `2 then A1: LeftComp (Cage (C,i)) c= LeftComp (Cage (C,j)) by JORDAN1H:47; A2: (W-bound (L~ (Cage (C,j)))) + (E-bound (L~ (Cage (C,j)))) = (W-bound C) + (E-bound C) by JORDAN1G:33; then A3: (LMP (L~ (Cage (C,j)))) `2 = lower_bound (proj2 .: ((L~ (Cage (C,j))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) by EUCLID:52; assume (LMP (L~ (Cage (C,i)))) `2 > (LMP (L~ (Cage (C,j)))) `2 ; ::_thesis: contradiction then A4: ((LMP (L~ (Cage (C,i)))) `2) - ((LMP (L~ (Cage (C,j)))) `2) > 0 by XREAL_1:50; A5: (W-bound (L~ (Cage (C,i)))) + (E-bound (L~ (Cage (C,i)))) = (W-bound C) + (E-bound C) by JORDAN1G:33; then A6: (LMP (L~ (Cage (C,i)))) `2 = lower_bound (proj2 .: ((L~ (Cage (C,i))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) by EUCLID:52; A7: ( not proj2 .: ((L~ (Cage (C,i))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is empty & proj2 .: ((L~ (Cage (C,i))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is bounded_below ) by A5, JORDAN21:12, JORDAN21:13; ( not proj2 .: ((L~ (Cage (C,j))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is empty & proj2 .: ((L~ (Cage (C,j))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is bounded_below ) by A2, JORDAN21:12, JORDAN21:13; then consider r being real number such that A8: r in proj2 .: ((L~ (Cage (C,j))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) and A9: r < (lower_bound (proj2 .: ((L~ (Cage (C,j))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))))) + (((LMP (L~ (Cage (C,i)))) `2) - ((LMP (L~ (Cage (C,j)))) `2)) by A4, SEQ_4:def_2; consider x being Point of (TOP-REAL 2) such that A10: x in (L~ (Cage (C,j))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) and A11: proj2 . x = r by A8, Lm1; A12: x `2 = r by A11, PSCOMP_1:def_6; south_halfline x misses L~ (Cage (C,i)) proof A13: x in Vertical_Line (((E-bound C) + (W-bound C)) / 2) by A10, XBOOLE_0:def_4; assume south_halfline x meets L~ (Cage (C,i)) ; ::_thesis: contradiction then consider y being set such that A14: y in south_halfline x and A15: y in L~ (Cage (C,i)) by XBOOLE_0:3; reconsider y = y as Point of (TOP-REAL 2) by A15; y `1 = x `1 by A14, TOPREAL1:def_12 .= ((E-bound C) + (W-bound C)) / 2 by A13, JORDAN6:31 ; then y in Vertical_Line (((E-bound C) + (W-bound C)) / 2) ; then A16: y in (L~ (Cage (C,i))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) by A15, XBOOLE_0:def_4; proj2 . y = y `2 by PSCOMP_1:def_6; then y `2 in proj2 .: ((L~ (Cage (C,i))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) by A16, FUNCT_2:35; then A17: y `2 >= (LMP (L~ (Cage (C,i)))) `2 by A6, A7, SEQ_4:def_2; y `2 <= x `2 by A14, TOPREAL1:def_12; hence contradiction by A3, A9, A12, A17, XXREAL_0:2; ::_thesis: verum end; then A18: south_halfline x c= UBD (L~ (Cage (C,i))) by JORDAN2C:128; x in south_halfline x by TOPREAL1:38; then x in UBD (L~ (Cage (C,i))) by A18; then A19: x in LeftComp (Cage (C,i)) by GOBRD14:36; x in L~ (Cage (C,j)) by A10, XBOOLE_0:def_4; then LeftComp (Cage (C,j)) meets L~ (Cage (C,j)) by A1, A19, XBOOLE_0:3; hence contradiction by SPRECT_3:26; ::_thesis: verum end; theorem Th27: :: JORDAN22:27 for C being Simple_closed_curve for i, j being Element of NAT st 0 < i & i <= j holds (UMP (Upper_Arc (L~ (Cage (C,j))))) `2 <= (UMP (Upper_Arc (L~ (Cage (C,i))))) `2 proof let C be Simple_closed_curve; ::_thesis: for i, j being Element of NAT st 0 < i & i <= j holds (UMP (Upper_Arc (L~ (Cage (C,j))))) `2 <= (UMP (Upper_Arc (L~ (Cage (C,i))))) `2 let i, j be Element of NAT ; ::_thesis: ( 0 < i & i <= j implies (UMP (Upper_Arc (L~ (Cage (C,j))))) `2 <= (UMP (Upper_Arc (L~ (Cage (C,i))))) `2 ) assume that A1: 0 < i and A2: i <= j ; ::_thesis: (UMP (Upper_Arc (L~ (Cage (C,j))))) `2 <= (UMP (Upper_Arc (L~ (Cage (C,i))))) `2 A3: (UMP (Upper_Arc (L~ (Cage (C,i))))) `2 = (UMP (L~ (Cage (C,i)))) `2 by A1, Th21; (UMP (Upper_Arc (L~ (Cage (C,j))))) `2 = (UMP (L~ (Cage (C,j)))) `2 by A1, A2, Th21; hence (UMP (Upper_Arc (L~ (Cage (C,j))))) `2 <= (UMP (Upper_Arc (L~ (Cage (C,i))))) `2 by A2, A3, Th25; ::_thesis: verum end; theorem Th28: :: JORDAN22:28 for C being Simple_closed_curve for i, j being Element of NAT st 0 < i & i <= j holds (LMP (Lower_Arc (L~ (Cage (C,i))))) `2 <= (LMP (Lower_Arc (L~ (Cage (C,j))))) `2 proof let C be Simple_closed_curve; ::_thesis: for i, j being Element of NAT st 0 < i & i <= j holds (LMP (Lower_Arc (L~ (Cage (C,i))))) `2 <= (LMP (Lower_Arc (L~ (Cage (C,j))))) `2 let i, j be Element of NAT ; ::_thesis: ( 0 < i & i <= j implies (LMP (Lower_Arc (L~ (Cage (C,i))))) `2 <= (LMP (Lower_Arc (L~ (Cage (C,j))))) `2 ) assume that A1: 0 < i and A2: i <= j ; ::_thesis: (LMP (Lower_Arc (L~ (Cage (C,i))))) `2 <= (LMP (Lower_Arc (L~ (Cage (C,j))))) `2 A3: (LMP (Lower_Arc (L~ (Cage (C,i))))) `2 = (LMP (L~ (Cage (C,i)))) `2 by A1, Th22; (LMP (Lower_Arc (L~ (Cage (C,j))))) `2 = (LMP (L~ (Cage (C,j)))) `2 by A1, A2, Th22; hence (LMP (Lower_Arc (L~ (Cage (C,i))))) `2 <= (LMP (Lower_Arc (L~ (Cage (C,j))))) `2 by A2, A3, Th26; ::_thesis: verum end; begin theorem Th29: :: JORDAN22:29 for C being Simple_closed_curve holds W-min C in North_Arc C proof let C be Simple_closed_curve; ::_thesis: W-min C in North_Arc C reconsider w = W-min C as Point of (Euclid 2) by EUCLID:67; A1: for r being real number st r > 0 holds ex k being Element of NAT st for m being Element of NAT st m > k holds (Upper_Appr C) . m meets Ball (w,r) proof let r be real number ; ::_thesis: ( r > 0 implies ex k being Element of NAT st for m being Element of NAT st m > k holds (Upper_Appr C) . m meets Ball (w,r) ) assume r > 0 ; ::_thesis: ex k being Element of NAT st for m being Element of NAT st m > k holds (Upper_Appr C) . m meets Ball (w,r) then r / 2 > 0 by XREAL_1:215; then consider k being Element of NAT such that 1 < k and A2: dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,2))) < r / 2 and A3: dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (2,1))) < r / 2 by GOBRD14:11; take k ; ::_thesis: for m being Element of NAT st m > k holds (Upper_Appr C) . m meets Ball (w,r) let m be Element of NAT ; ::_thesis: ( m > k implies (Upper_Appr C) . m meets Ball (w,r) ) assume A4: m > k ; ::_thesis: (Upper_Appr C) . m meets Ball (w,r) dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,2))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,2))) by A4, Th9; then A5: dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,2))) < r / 2 by A2, XXREAL_0:2; dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (2,1))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (2,1))) by A4, Th11; then A6: dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (2,1))) < r / 2 by A3, XXREAL_0:2; A7: 1 + 1 <= len (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))) by GOBOARD7:34, XXREAL_0:2; then A8: (left_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1)) /\ (right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1)) = LSeg ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1) by GOBOARD5:31; reconsider p = W-min (L~ (Cage (C,m))) as Point of (Euclid 2) by EUCLID:67; A9: W-min (L~ (Cage (C,m))) in Upper_Arc (L~ (Cage (C,m))) by JORDAN7:1; Cage (C,m) is_sequence_on Gauge (C,m) by JORDAN9:def_1; then A10: Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m))))) is_sequence_on Gauge (C,m) by REVROT_1:34; W-min (L~ (Cage (C,m))) in rng (Cage (C,m)) by SPRECT_2:43; then A11: W-min (L~ (Cage (C,m))) = (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))) /. 1 by FINSEQ_6:92; then (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))) /. 1 = W-min (L~ (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m))))))) by REVROT_1:33; then consider i, j being Element of NAT such that A12: [i,j] in Indices (Gauge (C,m)) and A13: [i,(j + 1)] in Indices (Gauge (C,m)) and A14: (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))) /. 1 = (Gauge (C,m)) * (i,j) and A15: (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))) /. (1 + 1) = (Gauge (C,m)) * (i,(j + 1)) by A7, A10, JORDAN1I:21; A16: 1 <= j by A12, MATRIX_1:38; i < len (Gauge (C,m)) by A7, A10, A12, A13, A14, A15, JORDAN1I:14; then A17: i + 1 <= len (Gauge (C,m)) by NAT_1:13; A18: 1 <= i + 1 by NAT_1:11; j <= width (Gauge (C,m)) by A12, MATRIX_1:38; then A19: [(i + 1),j] in Indices (Gauge (C,m)) by A16, A18, A17, MATRIX_1:36; [(1 + 1),1] in Indices (Gauge (C,m)) by Th7; then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * ((1 + 1),1))) = ((E-bound C) - (W-bound C)) / (2 |^ m) by Th5, GOBRD14:10; then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * ((1 + 1),1))) = dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * ((i + 1),j))) by A12, A19, GOBRD14:10; then A20: (((Gauge (C,m)) * ((i + 1),j)) `1) - (((Gauge (C,m)) * (i,j)) `1) < r / 2 by A12, A19, A6, GOBRD14:5; [1,(1 + 1)] in Indices (Gauge (C,m)) by Th6; then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,(1 + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ m) by Th5, GOBRD14:9; then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,(1 + 1)))) = dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * (i,(j + 1)))) by A12, A13, GOBRD14:9; then (((Gauge (C,m)) * (i,(j + 1))) `2) - (((Gauge (C,m)) * (i,j)) `2) < r / 2 by A12, A13, A5, GOBRD14:6; then A21: ((((Gauge (C,m)) * ((i + 1),j)) `1) - (((Gauge (C,m)) * (i,j)) `1)) + ((((Gauge (C,m)) * (i,(j + 1))) `2) - (((Gauge (C,m)) * (i,j)) `2)) < (r / 2) + (r / 2) by A20, XREAL_1:8; A22: 1 <= i by A12, MATRIX_1:38; right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1) = right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1,(GoB (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))))) by A7, JORDAN1H:23 .= right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1,(GoB (Cage (C,m)))) by REVROT_1:28 .= right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1,(Gauge (C,m))) by JORDAN1H:44 ; then A23: right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1) = cell ((Gauge (C,m)),i,j) by A7, A10, A12, A13, A14, A15, GOBRD13:22; A24: j + 1 <= width (Gauge (C,m)) by A13, MATRIX_1:38; (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))) /. 1 in LSeg ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1) by A7, TOPREAL1:21; then A25: W-min (L~ (Cage (C,m))) in right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1) by A11, A8, XBOOLE_0:def_4; then A26: ((Gauge (C,m)) * (i,j)) `1 <= (W-min (L~ (Cage (C,m)))) `1 by A23, A22, A16, A24, A17, JORDAN9:17; A27: W-min C in right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1) by JORDAN1I:6; then A28: (W-min C) `1 <= ((Gauge (C,m)) * ((i + 1),j)) `1 by A23, A22, A16, A24, A17, JORDAN9:17; A29: ((Gauge (C,m)) * (i,j)) `2 <= (W-min (L~ (Cage (C,m)))) `2 by A25, A23, A22, A16, A24, A17, JORDAN9:17; A30: (W-min (L~ (Cage (C,m)))) `1 <= ((Gauge (C,m)) * ((i + 1),j)) `1 by A25, A23, A22, A16, A24, A17, JORDAN9:17; A31: (W-min (L~ (Cage (C,m)))) `2 <= ((Gauge (C,m)) * (i,(j + 1))) `2 by A25, A23, A22, A16, A24, A17, JORDAN9:17; A32: (W-min C) `2 <= ((Gauge (C,m)) * (i,(j + 1))) `2 by A27, A23, A22, A16, A24, A17, JORDAN9:17; A33: ((Gauge (C,m)) * (i,j)) `2 <= (W-min C) `2 by A27, A23, A22, A16, A24, A17, JORDAN9:17; ((Gauge (C,m)) * (i,j)) `1 <= (W-min C) `1 by A27, A23, A22, A16, A24, A17, JORDAN9:17; then dist ((W-min C),(W-min (L~ (Cage (C,m))))) <= ((((Gauge (C,m)) * ((i + 1),j)) `1) - (((Gauge (C,m)) * (i,j)) `1)) + ((((Gauge (C,m)) * (i,(j + 1))) `2) - (((Gauge (C,m)) * (i,j)) `2)) by A28, A33, A32, A26, A30, A29, A31, TOPREAL6:95; then dist ((W-min C),(W-min (L~ (Cage (C,m))))) < r by A21, XXREAL_0:2; then dist (w,p) < r by TOPREAL6:def_1; then A34: p in Ball (w,r) by METRIC_1:11; (Upper_Appr C) . m = Upper_Arc (L~ (Cage (C,m))) by JORDAN19:def_1; hence (Upper_Appr C) . m meets Ball (w,r) by A9, A34, XBOOLE_0:3; ::_thesis: verum end; North_Arc C = Lim_inf (Upper_Appr C) by JORDAN19:def_3; hence W-min C in North_Arc C by A1, KURATO_2:14; ::_thesis: verum end; theorem Th30: :: JORDAN22:30 for C being Simple_closed_curve holds E-max C in North_Arc C proof let C be Simple_closed_curve; ::_thesis: E-max C in North_Arc C reconsider w = E-max C as Point of (Euclid 2) by EUCLID:67; A1: for r being real number st r > 0 holds ex k being Element of NAT st for m being Element of NAT st m > k holds (Upper_Appr C) . m meets Ball (w,r) proof let r be real number ; ::_thesis: ( r > 0 implies ex k being Element of NAT st for m being Element of NAT st m > k holds (Upper_Appr C) . m meets Ball (w,r) ) assume r > 0 ; ::_thesis: ex k being Element of NAT st for m being Element of NAT st m > k holds (Upper_Appr C) . m meets Ball (w,r) then r / 2 > 0 by XREAL_1:215; then consider k being Element of NAT such that 1 < k and A2: dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,2))) < r / 2 and A3: dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (2,1))) < r / 2 by GOBRD14:11; take k ; ::_thesis: for m being Element of NAT st m > k holds (Upper_Appr C) . m meets Ball (w,r) let m be Element of NAT ; ::_thesis: ( m > k implies (Upper_Appr C) . m meets Ball (w,r) ) assume A4: m > k ; ::_thesis: (Upper_Appr C) . m meets Ball (w,r) dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,2))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,2))) by A4, Th9; then A5: dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,2))) < r / 2 by A2, XXREAL_0:2; dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (2,1))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (2,1))) by A4, Th11; then A6: dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (2,1))) < r / 2 by A3, XXREAL_0:2; reconsider p = E-max (L~ (Cage (C,m))) as Point of (Euclid 2) by EUCLID:67; A7: E-max (L~ (Cage (C,m))) in Upper_Arc (L~ (Cage (C,m))) by JORDAN7:1; A8: 1 + 1 <= len (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))) by GOBOARD7:34, XXREAL_0:2; then A9: (left_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1)) /\ (right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1)) = LSeg ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1) by GOBOARD5:31; Cage (C,m) is_sequence_on Gauge (C,m) by JORDAN9:def_1; then A10: Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m))))) is_sequence_on Gauge (C,m) by REVROT_1:34; E-max (L~ (Cage (C,m))) in rng (Cage (C,m)) by SPRECT_2:46; then A11: E-max (L~ (Cage (C,m))) = (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))) /. 1 by FINSEQ_6:92; then (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))) /. 1 = E-max (L~ (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m))))))) by REVROT_1:33; then consider i, j being Element of NAT such that A12: [i,(j + 1)] in Indices (Gauge (C,m)) and A13: [i,j] in Indices (Gauge (C,m)) and A14: (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))) /. 1 = (Gauge (C,m)) * (i,(j + 1)) and A15: (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))) /. (1 + 1) = (Gauge (C,m)) * (i,j) by A8, A10, JORDAN1I:23; A16: i <= len (Gauge (C,m)) by A12, MATRIX_1:38; i > 1 by A8, A10, A12, A13, A14, A15, JORDAN1I:16; then A17: i - 1 > 1 - 1 by XREAL_1:14; then A18: i -' 1 = i - 1 by XREAL_0:def_2; then A19: i -' 1 <= len (Gauge (C,m)) by A16, XREAL_1:146, XXREAL_0:2; i - 1 is Element of NAT by A17, INT_1:3; then A20: i - 1 >= 0 + 1 by A17, NAT_1:13; then A21: (i -' 1) + 1 = i by NAT_D:43; right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1) = right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1,(GoB (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))))) by A8, JORDAN1H:23 .= right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1,(GoB (Cage (C,m)))) by REVROT_1:28 .= right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1,(Gauge (C,m))) by JORDAN1H:44 ; then A22: right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1) = cell ((Gauge (C,m)),(i -' 1),j) by A8, A10, A12, A13, A14, A15, GOBRD13:28; A23: j + 1 <= width (Gauge (C,m)) by A12, MATRIX_1:38; 1 <= j + 1 by NAT_1:11; then A24: [(i -' 1),(j + 1)] in Indices (Gauge (C,m)) by A23, A20, A18, A19, MATRIX_1:36; A25: 1 <= j by A13, MATRIX_1:38; j <= width (Gauge (C,m)) by A13, MATRIX_1:38; then A26: [(i -' 1),j] in Indices (Gauge (C,m)) by A25, A20, A18, A19, MATRIX_1:36; [1,(1 + 1)] in Indices (Gauge (C,m)) by Th6; then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,(1 + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ m) by Th5, GOBRD14:9; then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,(1 + 1)))) = dist (((Gauge (C,m)) * ((i -' 1),j)),((Gauge (C,m)) * ((i -' 1),(j + 1)))) by A26, A24, GOBRD14:9; then A27: (((Gauge (C,m)) * ((i -' 1),(j + 1))) `2) - (((Gauge (C,m)) * ((i -' 1),j)) `2) < r / 2 by A26, A24, A5, GOBRD14:6; [(1 + 1),1] in Indices (Gauge (C,m)) by Th7; then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * ((1 + 1),1))) = ((E-bound C) - (W-bound C)) / (2 |^ m) by Th5, GOBRD14:10; then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * ((1 + 1),1))) = dist (((Gauge (C,m)) * ((i -' 1),j)),((Gauge (C,m)) * (((i -' 1) + 1),j))) by A13, A21, A26, GOBRD14:10; then (((Gauge (C,m)) * (((i -' 1) + 1),j)) `1) - (((Gauge (C,m)) * ((i -' 1),j)) `1) < r / 2 by A13, A21, A26, A6, GOBRD14:5; then A28: ((((Gauge (C,m)) * (((i -' 1) + 1),j)) `1) - (((Gauge (C,m)) * ((i -' 1),j)) `1)) + ((((Gauge (C,m)) * ((i -' 1),(j + 1))) `2) - (((Gauge (C,m)) * ((i -' 1),j)) `2)) < (r / 2) + (r / 2) by A27, XREAL_1:8; A29: E-max C in right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1) by JORDAN1I:7; then A30: (E-max C) `1 <= ((Gauge (C,m)) * (((i -' 1) + 1),j)) `1 by A22, A25, A23, A20, A21, A16, JORDAN9:17; (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))) /. 1 in LSeg ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1) by A8, TOPREAL1:21; then A31: E-max (L~ (Cage (C,m))) in right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1) by A11, A9, XBOOLE_0:def_4; then A32: ((Gauge (C,m)) * ((i -' 1),j)) `1 <= (E-max (L~ (Cage (C,m)))) `1 by A22, A25, A23, A20, A21, A16, JORDAN9:17; A33: ((Gauge (C,m)) * ((i -' 1),j)) `2 <= (E-max (L~ (Cage (C,m)))) `2 by A31, A22, A25, A23, A20, A21, A16, JORDAN9:17; A34: (E-max (L~ (Cage (C,m)))) `1 <= ((Gauge (C,m)) * (((i -' 1) + 1),j)) `1 by A31, A22, A25, A23, A20, A21, A16, JORDAN9:17; A35: (E-max (L~ (Cage (C,m)))) `2 <= ((Gauge (C,m)) * ((i -' 1),(j + 1))) `2 by A31, A22, A25, A23, A20, A21, A16, JORDAN9:17; A36: (E-max C) `2 <= ((Gauge (C,m)) * ((i -' 1),(j + 1))) `2 by A29, A22, A25, A23, A20, A21, A16, JORDAN9:17; A37: ((Gauge (C,m)) * ((i -' 1),j)) `2 <= (E-max C) `2 by A29, A22, A25, A23, A20, A21, A16, JORDAN9:17; ((Gauge (C,m)) * ((i -' 1),j)) `1 <= (E-max C) `1 by A29, A22, A25, A23, A20, A21, A16, JORDAN9:17; then dist ((E-max C),(E-max (L~ (Cage (C,m))))) <= ((((Gauge (C,m)) * (((i -' 1) + 1),j)) `1) - (((Gauge (C,m)) * ((i -' 1),j)) `1)) + ((((Gauge (C,m)) * ((i -' 1),(j + 1))) `2) - (((Gauge (C,m)) * ((i -' 1),j)) `2)) by A30, A37, A36, A32, A34, A33, A35, TOPREAL6:95; then dist ((E-max C),(E-max (L~ (Cage (C,m))))) < r by A28, XXREAL_0:2; then dist (w,p) < r by TOPREAL6:def_1; then A38: p in Ball (w,r) by METRIC_1:11; (Upper_Appr C) . m = Upper_Arc (L~ (Cage (C,m))) by JORDAN19:def_1; hence (Upper_Appr C) . m meets Ball (w,r) by A7, A38, XBOOLE_0:3; ::_thesis: verum end; North_Arc C = Lim_inf (Upper_Appr C) by JORDAN19:def_3; hence E-max C in North_Arc C by A1, KURATO_2:14; ::_thesis: verum end; theorem Th31: :: JORDAN22:31 for C being Simple_closed_curve holds W-min C in South_Arc C proof let C be Simple_closed_curve; ::_thesis: W-min C in South_Arc C reconsider w = W-min C as Point of (Euclid 2) by EUCLID:67; A1: for r being real number st r > 0 holds ex k being Element of NAT st for m being Element of NAT st m > k holds (Lower_Appr C) . m meets Ball (w,r) proof let r be real number ; ::_thesis: ( r > 0 implies ex k being Element of NAT st for m being Element of NAT st m > k holds (Lower_Appr C) . m meets Ball (w,r) ) assume r > 0 ; ::_thesis: ex k being Element of NAT st for m being Element of NAT st m > k holds (Lower_Appr C) . m meets Ball (w,r) then r / 2 > 0 by XREAL_1:215; then consider k being Element of NAT such that 1 < k and A2: dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,2))) < r / 2 and A3: dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (2,1))) < r / 2 by GOBRD14:11; take k ; ::_thesis: for m being Element of NAT st m > k holds (Lower_Appr C) . m meets Ball (w,r) let m be Element of NAT ; ::_thesis: ( m > k implies (Lower_Appr C) . m meets Ball (w,r) ) assume A4: m > k ; ::_thesis: (Lower_Appr C) . m meets Ball (w,r) dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,2))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,2))) by A4, Th9; then A5: dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,2))) < r / 2 by A2, XXREAL_0:2; dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (2,1))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (2,1))) by A4, Th11; then A6: dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (2,1))) < r / 2 by A3, XXREAL_0:2; A7: 1 + 1 <= len (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))) by GOBOARD7:34, XXREAL_0:2; then A8: (left_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1)) /\ (right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1)) = LSeg ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1) by GOBOARD5:31; reconsider p = W-min (L~ (Cage (C,m))) as Point of (Euclid 2) by EUCLID:67; A9: W-min (L~ (Cage (C,m))) in Lower_Arc (L~ (Cage (C,m))) by JORDAN7:1; Cage (C,m) is_sequence_on Gauge (C,m) by JORDAN9:def_1; then A10: Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m))))) is_sequence_on Gauge (C,m) by REVROT_1:34; W-min (L~ (Cage (C,m))) in rng (Cage (C,m)) by SPRECT_2:43; then A11: W-min (L~ (Cage (C,m))) = (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))) /. 1 by FINSEQ_6:92; then (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))) /. 1 = W-min (L~ (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m))))))) by REVROT_1:33; then consider i, j being Element of NAT such that A12: [i,j] in Indices (Gauge (C,m)) and A13: [i,(j + 1)] in Indices (Gauge (C,m)) and A14: (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))) /. 1 = (Gauge (C,m)) * (i,j) and A15: (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))) /. (1 + 1) = (Gauge (C,m)) * (i,(j + 1)) by A7, A10, JORDAN1I:21; A16: 1 <= j by A12, MATRIX_1:38; i < len (Gauge (C,m)) by A7, A10, A12, A13, A14, A15, JORDAN1I:14; then A17: i + 1 <= len (Gauge (C,m)) by NAT_1:13; A18: 1 <= i + 1 by NAT_1:11; j <= width (Gauge (C,m)) by A12, MATRIX_1:38; then A19: [(i + 1),j] in Indices (Gauge (C,m)) by A16, A18, A17, MATRIX_1:36; [(1 + 1),1] in Indices (Gauge (C,m)) by Th7; then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * ((1 + 1),1))) = ((E-bound C) - (W-bound C)) / (2 |^ m) by Th5, GOBRD14:10; then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * ((1 + 1),1))) = dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * ((i + 1),j))) by A12, A19, GOBRD14:10; then A20: (((Gauge (C,m)) * ((i + 1),j)) `1) - (((Gauge (C,m)) * (i,j)) `1) < r / 2 by A12, A19, A6, GOBRD14:5; [1,(1 + 1)] in Indices (Gauge (C,m)) by Th6; then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,(1 + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ m) by Th5, GOBRD14:9; then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,(1 + 1)))) = dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * (i,(j + 1)))) by A12, A13, GOBRD14:9; then (((Gauge (C,m)) * (i,(j + 1))) `2) - (((Gauge (C,m)) * (i,j)) `2) < r / 2 by A12, A13, A5, GOBRD14:6; then A21: ((((Gauge (C,m)) * ((i + 1),j)) `1) - (((Gauge (C,m)) * (i,j)) `1)) + ((((Gauge (C,m)) * (i,(j + 1))) `2) - (((Gauge (C,m)) * (i,j)) `2)) < (r / 2) + (r / 2) by A20, XREAL_1:8; A22: 1 <= i by A12, MATRIX_1:38; right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1) = right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1,(GoB (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))))) by A7, JORDAN1H:23 .= right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1,(GoB (Cage (C,m)))) by REVROT_1:28 .= right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1,(Gauge (C,m))) by JORDAN1H:44 ; then A23: right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1) = cell ((Gauge (C,m)),i,j) by A7, A10, A12, A13, A14, A15, GOBRD13:22; A24: j + 1 <= width (Gauge (C,m)) by A13, MATRIX_1:38; (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))) /. 1 in LSeg ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1) by A7, TOPREAL1:21; then A25: W-min (L~ (Cage (C,m))) in right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1) by A11, A8, XBOOLE_0:def_4; then A26: ((Gauge (C,m)) * (i,j)) `1 <= (W-min (L~ (Cage (C,m)))) `1 by A23, A22, A16, A24, A17, JORDAN9:17; A27: W-min C in right_cell ((Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1) by JORDAN1I:6; then A28: (W-min C) `1 <= ((Gauge (C,m)) * ((i + 1),j)) `1 by A23, A22, A16, A24, A17, JORDAN9:17; A29: ((Gauge (C,m)) * (i,j)) `2 <= (W-min (L~ (Cage (C,m)))) `2 by A25, A23, A22, A16, A24, A17, JORDAN9:17; A30: (W-min (L~ (Cage (C,m)))) `1 <= ((Gauge (C,m)) * ((i + 1),j)) `1 by A25, A23, A22, A16, A24, A17, JORDAN9:17; A31: (W-min (L~ (Cage (C,m)))) `2 <= ((Gauge (C,m)) * (i,(j + 1))) `2 by A25, A23, A22, A16, A24, A17, JORDAN9:17; A32: (W-min C) `2 <= ((Gauge (C,m)) * (i,(j + 1))) `2 by A27, A23, A22, A16, A24, A17, JORDAN9:17; A33: ((Gauge (C,m)) * (i,j)) `2 <= (W-min C) `2 by A27, A23, A22, A16, A24, A17, JORDAN9:17; ((Gauge (C,m)) * (i,j)) `1 <= (W-min C) `1 by A27, A23, A22, A16, A24, A17, JORDAN9:17; then dist ((W-min C),(W-min (L~ (Cage (C,m))))) <= ((((Gauge (C,m)) * ((i + 1),j)) `1) - (((Gauge (C,m)) * (i,j)) `1)) + ((((Gauge (C,m)) * (i,(j + 1))) `2) - (((Gauge (C,m)) * (i,j)) `2)) by A28, A33, A32, A26, A30, A29, A31, TOPREAL6:95; then dist ((W-min C),(W-min (L~ (Cage (C,m))))) < r by A21, XXREAL_0:2; then dist (w,p) < r by TOPREAL6:def_1; then A34: p in Ball (w,r) by METRIC_1:11; (Lower_Appr C) . m = Lower_Arc (L~ (Cage (C,m))) by JORDAN19:def_2; hence (Lower_Appr C) . m meets Ball (w,r) by A9, A34, XBOOLE_0:3; ::_thesis: verum end; South_Arc C = Lim_inf (Lower_Appr C) by JORDAN19:def_4; hence W-min C in South_Arc C by A1, KURATO_2:14; ::_thesis: verum end; theorem Th32: :: JORDAN22:32 for C being Simple_closed_curve holds E-max C in South_Arc C proof let C be Simple_closed_curve; ::_thesis: E-max C in South_Arc C reconsider w = E-max C as Point of (Euclid 2) by EUCLID:67; A1: for r being real number st r > 0 holds ex k being Element of NAT st for m being Element of NAT st m > k holds (Lower_Appr C) . m meets Ball (w,r) proof let r be real number ; ::_thesis: ( r > 0 implies ex k being Element of NAT st for m being Element of NAT st m > k holds (Lower_Appr C) . m meets Ball (w,r) ) assume r > 0 ; ::_thesis: ex k being Element of NAT st for m being Element of NAT st m > k holds (Lower_Appr C) . m meets Ball (w,r) then r / 2 > 0 by XREAL_1:215; then consider k being Element of NAT such that 1 < k and A2: dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,2))) < r / 2 and A3: dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (2,1))) < r / 2 by GOBRD14:11; take k ; ::_thesis: for m being Element of NAT st m > k holds (Lower_Appr C) . m meets Ball (w,r) let m be Element of NAT ; ::_thesis: ( m > k implies (Lower_Appr C) . m meets Ball (w,r) ) assume A4: m > k ; ::_thesis: (Lower_Appr C) . m meets Ball (w,r) dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,2))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,2))) by A4, Th9; then A5: dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,2))) < r / 2 by A2, XXREAL_0:2; dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (2,1))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (2,1))) by A4, Th11; then A6: dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (2,1))) < r / 2 by A3, XXREAL_0:2; reconsider p = E-max (L~ (Cage (C,m))) as Point of (Euclid 2) by EUCLID:67; A7: E-max (L~ (Cage (C,m))) in Lower_Arc (L~ (Cage (C,m))) by JORDAN7:1; A8: 1 + 1 <= len (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))) by GOBOARD7:34, XXREAL_0:2; then A9: (left_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1)) /\ (right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1)) = LSeg ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1) by GOBOARD5:31; Cage (C,m) is_sequence_on Gauge (C,m) by JORDAN9:def_1; then A10: Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m))))) is_sequence_on Gauge (C,m) by REVROT_1:34; E-max (L~ (Cage (C,m))) in rng (Cage (C,m)) by SPRECT_2:46; then A11: E-max (L~ (Cage (C,m))) = (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))) /. 1 by FINSEQ_6:92; then (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))) /. 1 = E-max (L~ (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m))))))) by REVROT_1:33; then consider i, j being Element of NAT such that A12: [i,(j + 1)] in Indices (Gauge (C,m)) and A13: [i,j] in Indices (Gauge (C,m)) and A14: (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))) /. 1 = (Gauge (C,m)) * (i,(j + 1)) and A15: (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))) /. (1 + 1) = (Gauge (C,m)) * (i,j) by A8, A10, JORDAN1I:23; A16: i <= len (Gauge (C,m)) by A12, MATRIX_1:38; i > 1 by A8, A10, A12, A13, A14, A15, JORDAN1I:16; then A17: i - 1 > 1 - 1 by XREAL_1:14; then A18: i -' 1 = i - 1 by XREAL_0:def_2; then A19: i -' 1 <= len (Gauge (C,m)) by A16, XREAL_1:146, XXREAL_0:2; i - 1 is Element of NAT by A17, INT_1:3; then A20: i - 1 >= 0 + 1 by A17, NAT_1:13; then A21: (i -' 1) + 1 = i by NAT_D:43; right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1) = right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1,(GoB (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))))) by A8, JORDAN1H:23 .= right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1,(GoB (Cage (C,m)))) by REVROT_1:28 .= right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1,(Gauge (C,m))) by JORDAN1H:44 ; then A22: right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1) = cell ((Gauge (C,m)),(i -' 1),j) by A8, A10, A12, A13, A14, A15, GOBRD13:28; A23: j + 1 <= width (Gauge (C,m)) by A12, MATRIX_1:38; 1 <= j + 1 by NAT_1:11; then A24: [(i -' 1),(j + 1)] in Indices (Gauge (C,m)) by A23, A20, A18, A19, MATRIX_1:36; A25: 1 <= j by A13, MATRIX_1:38; j <= width (Gauge (C,m)) by A13, MATRIX_1:38; then A26: [(i -' 1),j] in Indices (Gauge (C,m)) by A25, A20, A18, A19, MATRIX_1:36; [1,(1 + 1)] in Indices (Gauge (C,m)) by Th6; then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,(1 + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ m) by Th5, GOBRD14:9; then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,(1 + 1)))) = dist (((Gauge (C,m)) * ((i -' 1),j)),((Gauge (C,m)) * ((i -' 1),(j + 1)))) by A26, A24, GOBRD14:9; then A27: (((Gauge (C,m)) * ((i -' 1),(j + 1))) `2) - (((Gauge (C,m)) * ((i -' 1),j)) `2) < r / 2 by A26, A24, A5, GOBRD14:6; [(1 + 1),1] in Indices (Gauge (C,m)) by Th7; then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * ((1 + 1),1))) = ((E-bound C) - (W-bound C)) / (2 |^ m) by Th5, GOBRD14:10; then dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * ((1 + 1),1))) = dist (((Gauge (C,m)) * ((i -' 1),j)),((Gauge (C,m)) * (((i -' 1) + 1),j))) by A13, A21, A26, GOBRD14:10; then (((Gauge (C,m)) * (((i -' 1) + 1),j)) `1) - (((Gauge (C,m)) * ((i -' 1),j)) `1) < r / 2 by A13, A21, A26, A6, GOBRD14:5; then A28: ((((Gauge (C,m)) * (((i -' 1) + 1),j)) `1) - (((Gauge (C,m)) * ((i -' 1),j)) `1)) + ((((Gauge (C,m)) * ((i -' 1),(j + 1))) `2) - (((Gauge (C,m)) * ((i -' 1),j)) `2)) < (r / 2) + (r / 2) by A27, XREAL_1:8; A29: E-max C in right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1) by JORDAN1I:7; then A30: (E-max C) `1 <= ((Gauge (C,m)) * (((i -' 1) + 1),j)) `1 by A22, A25, A23, A20, A21, A16, JORDAN9:17; (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))) /. 1 in LSeg ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1) by A8, TOPREAL1:21; then A31: E-max (L~ (Cage (C,m))) in right_cell ((Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1) by A11, A9, XBOOLE_0:def_4; then A32: ((Gauge (C,m)) * ((i -' 1),j)) `1 <= (E-max (L~ (Cage (C,m)))) `1 by A22, A25, A23, A20, A21, A16, JORDAN9:17; A33: ((Gauge (C,m)) * ((i -' 1),j)) `2 <= (E-max (L~ (Cage (C,m)))) `2 by A31, A22, A25, A23, A20, A21, A16, JORDAN9:17; A34: (E-max (L~ (Cage (C,m)))) `1 <= ((Gauge (C,m)) * (((i -' 1) + 1),j)) `1 by A31, A22, A25, A23, A20, A21, A16, JORDAN9:17; A35: (E-max (L~ (Cage (C,m)))) `2 <= ((Gauge (C,m)) * ((i -' 1),(j + 1))) `2 by A31, A22, A25, A23, A20, A21, A16, JORDAN9:17; A36: (E-max C) `2 <= ((Gauge (C,m)) * ((i -' 1),(j + 1))) `2 by A29, A22, A25, A23, A20, A21, A16, JORDAN9:17; A37: ((Gauge (C,m)) * ((i -' 1),j)) `2 <= (E-max C) `2 by A29, A22, A25, A23, A20, A21, A16, JORDAN9:17; ((Gauge (C,m)) * ((i -' 1),j)) `1 <= (E-max C) `1 by A29, A22, A25, A23, A20, A21, A16, JORDAN9:17; then dist ((E-max C),(E-max (L~ (Cage (C,m))))) <= ((((Gauge (C,m)) * (((i -' 1) + 1),j)) `1) - (((Gauge (C,m)) * ((i -' 1),j)) `1)) + ((((Gauge (C,m)) * ((i -' 1),(j + 1))) `2) - (((Gauge (C,m)) * ((i -' 1),j)) `2)) by A30, A37, A36, A32, A34, A33, A35, TOPREAL6:95; then dist ((E-max C),(E-max (L~ (Cage (C,m))))) < r by A28, XXREAL_0:2; then dist (w,p) < r by TOPREAL6:def_1; then A38: p in Ball (w,r) by METRIC_1:11; (Lower_Appr C) . m = Lower_Arc (L~ (Cage (C,m))) by JORDAN19:def_2; hence (Lower_Appr C) . m meets Ball (w,r) by A7, A38, XBOOLE_0:3; ::_thesis: verum end; South_Arc C = Lim_inf (Lower_Appr C) by JORDAN19:def_4; hence E-max C in South_Arc C by A1, KURATO_2:14; ::_thesis: verum end; Lm4: TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by EUCLID:def_8; theorem Th33: :: JORDAN22:33 for C being Simple_closed_curve holds UMP C in North_Arc C proof 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 } ; 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 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 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 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 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 by XXREAL_2:def_11; A11: (UMP C) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52; A12: 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)))); 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; percases ( 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)))]| ) ; supposeA25: 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 percases ( (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 number 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 set 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 by XREAL_1:215; then consider k being Element of 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 Element of 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 Element of 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_1:38; right_cell ((Cage (C,k)),i,(Gauge (C,k))) meets C by A54, A55, JORDAN9:31; then consider c being set 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_1:38; (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_1:38; A71: (j2 + 1) + 1 <> j2 ; A72: 1 <= i2 by A60, MATRIX_1:38; A73: j1 <= width (Gauge (C,k)) by A58, MATRIX_1:38; A74: 1 <= j1 + 1 by NAT_1:11; A75: i1 + 1 <> i1 + 0 ; A76: i1 <= len (Gauge (C,k)) by A58, MATRIX_1:38; A77: i2 <= len (Gauge (C,k)) by A60, MATRIX_1:38; A78: (i2 + 1) + 1 <> i2 ; A79: 1 <= j1 by A58, MATRIX_1:38; A80: 1 <= i1 + 1 by NAT_1:11; now__::_thesis:_contradiction percases ( ( 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; supposeA81: ( 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_1:36; 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_1:38; 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; supposeA97: ( 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_1:36; 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_1:36; 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_1:38; 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; supposeA116: ( 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_1:38; 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_1:36; 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; supposeA132: ( 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_1:36; A136: [(i1 -' 1),(j2 + 1)] in Indices (Gauge (C,k)) by A79, A73, A132, A133, A134, MATRIX_1:36; 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_1:38; 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_1:36; 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 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 ; deffunc H1( Element of 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 Function of NAT,(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 Element of 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 ext-real number ; :: 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 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 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 Element of NAT st for m being Element of NAT st n <= m holds |.((S . m) - pp).| < r proof A159: 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 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 Element of 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 Element of NAT st for m being Element of NAT st n <= m holds |.((S . m) - pp).| < r ) assume 0 < r ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((S . m) - pp).| < r then consider v being real number 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 Element of 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 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 ) reconsider Sm = S . m as Element of (TOP-REAL 2) by EUCLID:22; assume A171: 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; then A172: (Sm `2) - ((UMP C) `2) <= v - ((UMP C) `2) by XREAL_1:13; reconsider SSm = Sm as Point of (TOP-REAL 2) ; A173: SSm - p1 = (S . m) - pp ; A174: S . m = UMP (Upper_Arc (L~ (Cage (C,m)))) by A155; then Sm `1 = ((W-bound C) + (E-bound C)) / 2 by A5; then abs ((Sm `1) - ((UMP C) `1)) = 0 by A11, ABSVALUE:def_1; then A175: |.((S . m) - pp).| <= 0 + (abs ((Sm `2) - ((UMP C) `2))) by A173, JGRAPH_1:32; 0 < (Sm `2) - ((UMP C) `2) by A170, A174, A171, Th23, XREAL_1:50; then A176: |.((S . m) - pp).| <= (Sm `2) - ((UMP C) `2) by A175, ABSVALUE:def_1; 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 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, A172, XXREAL_0:2; hence |.((S . m) - pp).| < r by A176, XXREAL_0:2; ::_thesis: verum end; thus A177: 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_8 ::_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 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 A178: for m being Element of NAT st n <= m holds |.((S . m) - pp).| < r by A158; 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 A178; hence |.((SS . m) - (UMP C)).| < r ; ::_thesis: verum end; hereby ::_thesis: UMP C = lim SS let x be Element of NAT ; ::_thesis: SS . x in (Upper_Appr C) . x A179: (Upper_Appr C) . x = Upper_Arc (L~ (Cage (C,x))) by JORDAN19:def_1; S . x = UMP (Upper_Arc (L~ (Cage (C,x)))) by A155; hence SS . x in (Upper_Appr C) . x by A179, JORDAN21:30; ::_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 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 A180: for m being Element of NAT st n <= m holds |.((S . m) - pp).| < r by A158; 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 A180; hence |.((SS . m) - (UMP C)).| < r ; ::_thesis: verum end; hence UMP C = lim SS by A177, 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; end; theorem Th34: :: JORDAN22:34 for C being Simple_closed_curve holds LMP C in South_Arc C proof let C be Simple_closed_curve; ::_thesis: LMP C in South_Arc C set w = ((W-bound C) + (E-bound C)) / 2; set p = LMP C; set U = { (LMP (Lower_Arc (L~ (Cage (C,n))))) where n is Element of NAT : 0 < n } ; set n0 = S-bound (L~ (Cage (C,1))); set H = LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|); A1: |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52; A2: |[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]| `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52; { (LMP (Lower_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 { (LMP (Lower_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 { (LMP (Lower_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 = LMP (Lower_Arc (L~ (Cage (C,n)))) & 0 < n ) ; hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum end; then reconsider U = { (LMP (Lower_Arc (L~ (Cage (C,n))))) where n is Element of NAT : 0 < n } as Subset of (TOP-REAL 2) ; set q = upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)); set S = LSeg (|[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|); A3: |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 = S-bound C by EUCLID:52; A4: |[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]| `2 = S-bound (L~ (Cage (C,1))) by EUCLID:52; A5: for n being Element of NAT holds (LMP (Lower_Arc (L~ (Cage (C,n))))) `1 = ((W-bound C) + (E-bound C)) / 2 proof let n be Element of NAT ; ::_thesis: (LMP (Lower_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 (LMP (Lower_Arc (L~ (Cage (C,n))))) `1 = ((W-bound (Lower_Arc (L~ (Cage (C,n))))) + (E-bound (Lower_Arc (L~ (Cage (C,n)))))) / 2 by EUCLID:52 .= ((W-bound (L~ (Cage (C,n)))) + (E-bound (Lower_Arc (L~ (Cage (C,n)))))) / 2 by JORDAN21:19 .= ((W-bound C) + (E-bound C)) / 2 by A6, JORDAN21:20 ; ::_thesis: verum end; A7: (LMP C) `2 >= (LMP (Lower_Arc (L~ (Cage (C,1))))) `2 by Th24; A8: (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ C = {(LMP C)} by JORDAN21:35; A9: (LMP (Lower_Arc (L~ (Cage (C,1))))) `2 >= S-bound (L~ (Cage (C,1))) by JORDAN21:48; (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U is bounded by TOPREAL6:89; then proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U) is real-bounded by JCT_MISC:14; then A10: proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U) is bounded_above by XXREAL_2:def_11; A11: (LMP C) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52; A12: for n being Element of NAT st 0 < n holds (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 in proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U) proof let n be Element of NAT ; ::_thesis: ( 0 < n implies (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 in proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U) ) set f = Cage (C,n); set s = LMP (Lower_Arc (L~ (Cage (C,n)))); assume A13: 0 < n ; ::_thesis: (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 in proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U) then A14: LMP (Lower_Arc (L~ (Cage (C,n)))) in U ; 0 + 1 <= n by A13, NAT_1:13; then ( n = 1 or n > 1 ) by XXREAL_0:1; then A15: S-bound (L~ (Cage (C,n))) >= S-bound (L~ (Cage (C,1))) by JORDAN1A:69; S-bound (L~ (Cage (C,n))) <= (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 by JORDAN21:48; then A16: (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 >= S-bound (L~ (Cage (C,1))) by A15, XXREAL_0:2; A17: (LMP (Lower_Arc (L~ (Cage (C,n))))) `1 = ((W-bound C) + (E-bound C)) / 2 by A5; (LMP C) `2 >= (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 by A13, Th24; then LMP (Lower_Arc (L~ (Cage (C,n)))) in LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|) by A2, A4, A11, A16, A17, GOBOARD7:7; then A18: LMP (Lower_Arc (L~ (Cage (C,n)))) in (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U by A14, XBOOLE_0:def_4; (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 = proj2 . (LMP (Lower_Arc (L~ (Cage (C,n))))) by PSCOMP_1:def_6; hence (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 in proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U) by A18, FUNCT_2:35; ::_thesis: verum end; then A19: (LMP (Lower_Arc (L~ (Cage (C,1))))) `2 in proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U) ; then upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) >= (LMP (Lower_Arc (L~ (Cage (C,1))))) `2 by A10, SEQ_4:def_1; then A20: upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) >= S-bound (L~ (Cage (C,1))) by A9, XXREAL_0:2; A21: |[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-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),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|) is vertical by A2, SPPOL_1:16; A23: |[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]| in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|) by RLTOPSP1:68; A24: |[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]| `2 = upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) by EUCLID:52; percases ( LMP C <> |[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]| or LMP C = |[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]| ) ; supposeA25: LMP C <> |[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]| ; ::_thesis: LMP C in South_Arc C consider S9, C9 being Subset of (TopSpaceMetr (Euclid 2)) such that A26: LSeg (|[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|) = S9 and A27: C = C9 and A28: dist_min ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(S-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_(LMP_C)_`2_<=_upper_bound_(proj2_.:_((LSeg_((LMP_C),|[(((W-bound_C)_+_(E-bound_C))_/_2),(S-bound_(L~_(Cage_(C,1))))]|))_/\_U)) assume A32: (LMP C) `2 <= upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) ; ::_thesis: contradiction percases ( (LMP C) `2 = upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) or (LMP C) `2 < upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) ) by A32, XXREAL_0:1; suppose (LMP C) `2 = upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) ; ::_thesis: contradiction hence contradiction by A25, EUCLID:52; ::_thesis: verum end; suppose (LMP C) `2 < upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) ; ::_thesis: contradiction then 0 < (upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U))) - ((LMP C) `2) by XREAL_1:50; then consider r being real number such that A33: r in proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U) and A34: (upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U))) - ((upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U))) - ((LMP C) `2)) < r by A10, A19, SEQ_4:def_1; consider t being Point of (TOP-REAL 2) such that A35: t in (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U and A36: proj2 . t = r by A33, Lm1; A37: t in LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|) by A35, XBOOLE_0:def_4; A38: (LMP C) `2 >= S-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),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|) misses C proof assume LSeg (|[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|) meets C ; ::_thesis: contradiction then consider x being set such that A39: x in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(S-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 >= S-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: upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) >= x `2 by A4, A24, A20, A39, TOPREAL1:4; then (LMP C) `2 > x `2 by A31, XXREAL_0:2; then x in LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) by A1, A3, A11, A41, A42, GOBOARD7:7; then x in {(LMP 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),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(S-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),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)),C)) / 2 > 0 by XREAL_1:215; then consider k being Element of 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),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(S-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),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)),C)) / 2 by GOBRD14:11; set f = Cage (C,k); set G = Gauge (C,k); set s = LMP (Lower_Arc (L~ (Cage (C,k)))); A47: (LMP (Lower_Arc (L~ (Cage (C,k))))) `2 >= S-bound (L~ (Cage (C,k))) by JORDAN21:48; 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),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)),C)) / 2) + ((dist_min ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)),C)) / 2) by A45, A46, XREAL_1:8; S-bound (L~ (Cage (C,k))) >= S-bound (L~ (Cage (C,1))) by A44, JORDAN1A:69; then A49: (LMP (Lower_Arc (L~ (Cage (C,k))))) `2 >= S-bound (L~ (Cage (C,1))) by A47, XXREAL_0:2; (LMP (Lower_Arc (L~ (Cage (C,k))))) `2 in proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U) by A12, A44; then A50: upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) >= (LMP (Lower_Arc (L~ (Cage (C,k))))) `2 by A10, SEQ_4:def_1; [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: LMP (Lower_Arc (L~ (Cage (C,k)))) in Lower_Arc (L~ (Cage (C,k))) by JORDAN21:31; Lower_Arc (L~ (Cage (C,k))) c= L~ (Cage (C,k)) by JORDAN6:61; then consider i being Element of NAT such that A54: 1 <= i and A55: i + 1 <= len (Cage (C,k)) and A56: LMP (Lower_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 Element of 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_1:38; right_cell ((Cage (C,k)),i,(Gauge (C,k))) meets C by A54, A55, JORDAN9:31; then consider c being set 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 = LMP (Lower_Arc (L~ (Cage (C,k)))), c9 = c as Point of (Euclid 2) by EUCLID:67; (LMP (Lower_Arc (L~ (Cage (C,k))))) `1 = ((W-bound C) + (E-bound C)) / 2 by A5; then LMP (Lower_Arc (L~ (Cage (C,k)))) in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]|,|[(((W-bound C) + (E-bound C)) / 2),(S-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 ((LMP (Lower_Arc (L~ (Cage (C,k))))),c) by TOPREAL6:def_1; A68: 1 <= j2 by A60, MATRIX_1:38; (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: LMP (Lower_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_1:38; A71: (j2 + 1) + 1 <> j2 ; A72: 1 <= i2 by A60, MATRIX_1:38; A73: j1 <= width (Gauge (C,k)) by A58, MATRIX_1:38; A74: 1 <= j1 + 1 by NAT_1:11; A75: i1 + 1 <> i1 + 0 ; A76: i1 <= len (Gauge (C,k)) by A58, MATRIX_1:38; A77: i2 <= len (Gauge (C,k)) by A60, MATRIX_1:38; A78: (i2 + 1) + 1 <> i2 ; A79: 1 <= j1 by A58, MATRIX_1:38; A80: 1 <= i1 + 1 by NAT_1:11; now__::_thesis:_contradiction percases ( ( 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; supposeA81: ( 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_1:36; 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_1:38; 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: (LMP (Lower_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 <= (LMP (Lower_Arc (L~ (Cage (C,k))))) `2 by A69, A63, A79, A88, A84, A89, JORDAN9:17; A93: (LMP (Lower_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 <= (LMP (Lower_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 ((LMP (Lower_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; supposeA97: ( 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_1:36; 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_1:36; 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_1:38; 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: (LMP (Lower_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 <= (LMP (Lower_Arc (L~ (Cage (C,k))))) `2 by A69, A63, A73, A107, A98, A99, A108, JORDAN9:17; A112: (LMP (Lower_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 <= (LMP (Lower_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 ((LMP (Lower_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; supposeA116: ( 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_1:38; 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_1:36; 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: (LMP (Lower_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 <= (LMP (Lower_Arc (L~ (Cage (C,k))))) `2 by A69, A79, A72, A116, A119, A120, A123, JORDAN9:17; A129: (LMP (Lower_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 <= (LMP (Lower_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 ((LMP (Lower_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; supposeA132: ( 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_1:36; A136: [(i1 -' 1),(j2 + 1)] in Indices (Gauge (C,k)) by A79, A73, A132, A133, A134, MATRIX_1:36; 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_1:38; 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_1:36; 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: (LMP (Lower_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 <= (LMP (Lower_Arc (L~ (Cage (C,k))))) `2 by A69, A68, A76, A139, A133, A140, A143, JORDAN9:17; A147: (LMP (Lower_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 <= (LMP (Lower_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 ((LMP (Lower_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 LMP C in South_Arc C ; ::_thesis: verum end; suppose LMP C = |[(((W-bound C) + (E-bound C)) / 2),(upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)))]| ; ::_thesis: LMP C in South_Arc C then A152: (LMP C) `2 = upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) by EUCLID:52; A153: ex S being Real_Sequence of 2 st ( S is convergent & ( for x being Element of NAT holds S . x in (Lower_Appr C) . x ) & LMP C = lim S ) proof set R = { ((LMP (Lower_Arc (L~ (Cage (C,n))))) `2) where n is Element of NAT : 0 < n } ; { ((LMP (Lower_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 { ((LMP (Lower_Arc (L~ (Cage (C,n))))) `2) where n is Element of NAT : 0 < n } or x in REAL ) assume x in { ((LMP (Lower_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 = (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 & 0 < n ) ; hence x in REAL ; ::_thesis: verum end; then reconsider R = { ((LMP (Lower_Arc (L~ (Cage (C,n))))) `2) where n is Element of NAT : 0 < n } as Subset of REAL ; deffunc H1( Element of NAT ) -> Element of the carrier of (TOP-REAL 2) = LMP (Lower_Arc (L~ (Cage (C,$1)))); reconsider pp = LMP C as Element of REAL 2 by EUCLID:22; A154: for x being Element of NAT holds H1(x) is Element of REAL 2 by EUCLID:22; consider S being Function of NAT,(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 Element of NAT holds SS . x in (Lower_Appr C) . x ) & LMP C = lim SS ) A156: R is bounded_above proof take upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) ; :: according to XXREAL_2:def_10 ::_thesis: upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) is UpperBound of R let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in R or r <= upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) ) assume r in R ; ::_thesis: r <= upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) then ex n being Element of NAT st ( r = (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 & 0 < n ) ; then r in proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U) by A12; hence r <= upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) by A10, SEQ_4:def_1; ::_thesis: verum end; A157: (LMP (Lower_Arc (L~ (Cage (C,1))))) `2 in R ; A158: 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 A159: for s being real number st 0 < s holds ex r being real number st ( r in R & (upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U))) - s < r ) proof let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st ( r in R & (upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U))) - s < r ) ) assume 0 < s ; ::_thesis: ex r being real number st ( r in R & (upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U))) - s < r ) then consider r being real number such that A160: r in proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U) and A161: (upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U))) - s < r by A10, A19, SEQ_4:def_1; take r ; ::_thesis: ( r in R & (upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U))) - s < r ) consider x being Point of (TOP-REAL 2) such that A162: x in (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-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 Element of NAT such that A164: x = LMP (Lower_Arc (L~ (Cage (C,n)))) and A165: 0 < n ; r = (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 by A163, A164, PSCOMP_1:def_6; hence ( r in R & (upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U))) - s < r ) by A161, A165; ::_thesis: verum end; reconsider p1 = LMP C as Element of (TOP-REAL 2) ; 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 0 < r ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((S . m) - pp).| < r then consider v being real number such that A166: v in R and A167: (upper_bound R) - r < v by A157, A156, SEQ_4:def_1; consider n being Element of NAT such that A168: v = (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 and A169: 0 < n by A166; ((upper_bound R) - r) + r < v + r by A167, XREAL_1:6; then A170: (upper_bound R) - v < (v + r) - v by XREAL_1:14; 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 ) reconsider Sm = S . m as Point of (TOP-REAL 2) by EUCLID:22; assume A171: n <= m ; ::_thesis: |.((S . m) - pp).| < r then (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 <= (LMP (Lower_Arc (L~ (Cage (C,m))))) `2 by A169, Th28; then Sm `2 >= v by A155, A168; then A172: ((LMP C) `2) - (Sm `2) <= ((LMP C) `2) - v by XREAL_1:13; reconsider SSm = Sm as Point of (TOP-REAL 2) ; A173: SSm - p1 = (S . m) - pp ; A174: S . m = LMP (Lower_Arc (L~ (Cage (C,m)))) by A155; then Sm `1 = ((W-bound C) + (E-bound C)) / 2 by A5; then abs ((Sm `1) - ((LMP C) `1)) = 0 by A11, ABSVALUE:def_1; then A175: |.((S . m) - pp).| <= 0 + (abs ((Sm `2) - ((LMP C) `2))) by A173, JGRAPH_1:32; 0 > (Sm `2) - ((LMP C) `2) by A169, A174, A171, Th24, XREAL_1:49; then A176: |.((S . m) - pp).| <= - ((Sm `2) - ((LMP C) `2)) by A175, ABSVALUE:def_1; for r being real number st r in R holds upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) >= r proof let r be real number ; ::_thesis: ( r in R implies upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) >= r ) assume r in R ; ::_thesis: upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) >= r then ex n being Element of NAT st ( r = (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 & 0 < n ) ; then r in proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U) by A12; hence upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) >= r by A10, SEQ_4:def_1; ::_thesis: verum end; then upper_bound R = upper_bound (proj2 .: ((LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|)) /\ U)) by A157, A156, A159, SEQ_4:def_1; then ((LMP C) `2) - (Sm `2) < r by A152, A170, A172, XXREAL_0:2; hence |.((S . m) - pp).| < r by A176, XXREAL_0:2; ::_thesis: verum end; thus A177: SS is convergent ::_thesis: ( ( for x being Element of NAT holds SS . x in (Lower_Appr C) . x ) & LMP C = lim SS ) proof take LMP C ; :: according to TOPRNS_1:def_8 ::_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) - (LMP 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) - (LMP C)).| ) ) assume 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) - (LMP C)).| ) then consider n being Element of NAT such that A178: for m being Element of NAT st n <= m holds |.((S . m) - pp).| < r by A158; take n ; ::_thesis: for b1 being Element of NAT holds ( not n <= b1 or not r <= |.((SS . b1) - (LMP C)).| ) let m be Element of NAT ; ::_thesis: ( not n <= m or not r <= |.((SS . m) - (LMP C)).| ) assume n <= m ; ::_thesis: not r <= |.((SS . m) - (LMP C)).| then |.((S . m) - pp).| < r by A178; hence |.((SS . m) - (LMP C)).| < r ; ::_thesis: verum end; hereby ::_thesis: LMP C = lim SS let x be Element of NAT ; ::_thesis: SS . x in (Lower_Appr C) . x A179: (Lower_Appr C) . x = Lower_Arc (L~ (Cage (C,x))) by JORDAN19:def_2; S . x = LMP (Lower_Arc (L~ (Cage (C,x)))) by A155; hence SS . x in (Lower_Appr C) . x by A179, JORDAN21:31; ::_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) - (LMP 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) - (LMP C)).| < r ) assume 0 < r ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((SS . m) - (LMP C)).| < r then consider n being Element of NAT such that A180: for m being Element of NAT st n <= m holds |.((S . m) - pp).| < r by A158; take n ; ::_thesis: for m being Element of NAT st n <= m holds |.((SS . m) - (LMP C)).| < r let m be Element of NAT ; ::_thesis: ( n <= m implies |.((SS . m) - (LMP C)).| < r ) assume n <= m ; ::_thesis: |.((SS . m) - (LMP C)).| < r then |.((S . m) - pp).| < r by A180; hence |.((SS . m) - (LMP C)).| < r ; ::_thesis: verum end; hence LMP C = lim SS by A177, TOPRNS_1:def_9; ::_thesis: verum end; South_Arc C = Lim_inf (Lower_Appr C) by JORDAN19:def_4; hence LMP C in South_Arc C by A153, KURATO_2:21; ::_thesis: verum end; end; end; theorem Th35: :: JORDAN22:35 for C being Simple_closed_curve holds North_Arc C c= C proof let C be Simple_closed_curve; ::_thesis: North_Arc C c= C A1: North_Arc C = Lim_inf (Upper_Appr C) by JORDAN19:def_3; reconsider OO = BDD C as Subset of (TopSpaceMetr (Euclid 2)) by Lm4; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in North_Arc C or x in C ) assume A2: x in North_Arc C ; ::_thesis: x in C assume A3: not x in C ; ::_thesis: contradiction reconsider x = x as Point of (TOP-REAL 2) by A2; A4: x in C ` by A3, SUBSET_1:29; A5: (BDD C) \/ (UBD C) = C ` by JORDAN2C:27; reconsider e = x as Point of (Euclid 2) by EUCLID:67; percases ( x in BDD C or x in UBD C ) by A4, A5, XBOOLE_0:def_3; supposeA6: x in BDD C ; ::_thesis: contradiction OO is open by Lm4, PRE_TOPC:30; then consider r being real number such that A7: r > 0 and A8: Ball (e,r) c= BDD C by A6, TOPMETR:15; consider k being Element of NAT such that A9: for m being Element of NAT st m > k holds (Upper_Appr C) . m meets Ball (e,r) by A2, A1, A7, KURATO_2:14; A10: Upper_Arc (L~ (Cage (C,(k + 1)))) c= L~ (Cage (C,(k + 1))) by JORDAN6:61; A11: (Upper_Appr C) . (k + 1) = Upper_Arc (L~ (Cage (C,(k + 1)))) by JORDAN19:def_1; A12: k + 0 < k + 1 by XREAL_1:8; Ball (e,r) misses L~ (Cage (C,(k + 1))) by A8, JORDAN10:19, XBOOLE_1:63; hence contradiction by A9, A12, A11, A10, XBOOLE_1:63; ::_thesis: verum end; supposeA13: x in UBD C ; ::_thesis: contradiction union (UBD-Family C) = UBD C by JORDAN10:14; then consider A being set such that A14: x in A and A15: A in UBD-Family C by A13, TARSKI:def_4; UBD-Family C = { (UBD (L~ (Cage (C,m)))) where m is Element of NAT : verum } by JORDAN10:def_1; then consider m being Element of NAT such that A16: A = UBD (L~ (Cage (C,m))) by A15; reconsider OO = LeftComp (Cage (C,m)) as Subset of (TopSpaceMetr (Euclid 2)) by Lm4; A17: OO is open by Lm4, PRE_TOPC:30; x in LeftComp (Cage (C,m)) by A14, A16, GOBRD14:36; then consider r being real number such that A18: r > 0 and A19: Ball (e,r) c= LeftComp (Cage (C,m)) by A17, TOPMETR:15; consider k being Element of NAT such that A20: for m being Element of NAT st m > k holds (Upper_Appr C) . m meets Ball (e,r) by A2, A1, A18, KURATO_2:14; thus contradiction ::_thesis: verum proof percases ( m > k or m <= k ) ; supposeA21: m > k ; ::_thesis: contradiction A22: (Upper_Appr C) . m = Upper_Arc (L~ (Cage (C,m))) by JORDAN19:def_1; A23: Upper_Arc (L~ (Cage (C,m))) c= L~ (Cage (C,m)) by JORDAN6:61; Ball (e,r) misses L~ (Cage (C,m)) by A19, SPRECT_3:26, XBOOLE_1:63; hence contradiction by A20, A21, A22, A23, XBOOLE_1:63; ::_thesis: verum end; suppose m <= k ; ::_thesis: contradiction then LeftComp (Cage (C,m)) c= LeftComp (Cage (C,k)) by JORDAN1H:47; then A24: Ball (e,r) c= LeftComp (Cage (C,k)) by A19, XBOOLE_1:1; A25: k + 0 < k + 1 by XREAL_1:8; then LeftComp (Cage (C,k)) c= LeftComp (Cage (C,(k + 1))) by JORDAN1H:47; then Ball (e,r) c= LeftComp (Cage (C,(k + 1))) by A24, XBOOLE_1:1; then A26: Ball (e,r) misses L~ (Cage (C,(k + 1))) by SPRECT_3:26, XBOOLE_1:63; A27: Upper_Arc (L~ (Cage (C,(k + 1)))) c= L~ (Cage (C,(k + 1))) by JORDAN6:61; (Upper_Appr C) . (k + 1) = Upper_Arc (L~ (Cage (C,(k + 1)))) by JORDAN19:def_1; hence contradiction by A20, A25, A26, A27, XBOOLE_1:63; ::_thesis: verum end; end; end; end; end; end; theorem Th36: :: JORDAN22:36 for C being Simple_closed_curve holds South_Arc C c= C proof let C be Simple_closed_curve; ::_thesis: South_Arc C c= C let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in South_Arc C or x in C ) assume A1: x in South_Arc C ; ::_thesis: x in C assume A2: not x in C ; ::_thesis: contradiction reconsider x = x as Point of (TOP-REAL 2) by A1; A3: x in C ` by A2, SUBSET_1:29; reconsider e = x as Point of (Euclid 2) by EUCLID:67; A4: South_Arc C = Lim_inf (Lower_Appr C) by JORDAN19:def_4; A5: (BDD C) \/ (UBD C) = C ` by JORDAN2C:27; percases ( x in BDD C or x in UBD C ) by A3, A5, XBOOLE_0:def_3; supposeA6: x in BDD C ; ::_thesis: contradiction reconsider OO = BDD C as Subset of (TopSpaceMetr (Euclid 2)) by Lm4; OO is open by Lm4, PRE_TOPC:30; then consider r being real number such that A7: r > 0 and A8: Ball (e,r) c= BDD C by A6, TOPMETR:15; consider k being Element of NAT such that A9: for m being Element of NAT st m > k holds (Lower_Appr C) . m meets Ball (e,r) by A1, A4, A7, KURATO_2:14; A10: Lower_Arc (L~ (Cage (C,(k + 1)))) c= L~ (Cage (C,(k + 1))) by JORDAN6:61; A11: (Lower_Appr C) . (k + 1) = Lower_Arc (L~ (Cage (C,(k + 1)))) by JORDAN19:def_2; A12: k + 0 < k + 1 by XREAL_1:8; Ball (e,r) misses L~ (Cage (C,(k + 1))) by A8, JORDAN10:19, XBOOLE_1:63; hence contradiction by A9, A12, A11, A10, XBOOLE_1:63; ::_thesis: verum end; supposeA13: x in UBD C ; ::_thesis: contradiction union (UBD-Family C) = UBD C by JORDAN10:14; then consider A being set such that A14: x in A and A15: A in UBD-Family C by A13, TARSKI:def_4; UBD-Family C = { (UBD (L~ (Cage (C,m)))) where m is Element of NAT : verum } by JORDAN10:def_1; then consider m being Element of NAT such that A16: A = UBD (L~ (Cage (C,m))) by A15; reconsider OO = LeftComp (Cage (C,m)) as Subset of (TopSpaceMetr (Euclid 2)) by Lm4; A17: OO is open by Lm4, PRE_TOPC:30; x in LeftComp (Cage (C,m)) by A14, A16, GOBRD14:36; then consider r being real number such that A18: r > 0 and A19: Ball (e,r) c= LeftComp (Cage (C,m)) by A17, TOPMETR:15; consider k being Element of NAT such that A20: for m being Element of NAT st m > k holds (Lower_Appr C) . m meets Ball (e,r) by A1, A4, A18, KURATO_2:14; thus contradiction ::_thesis: verum proof percases ( m > k or m <= k ) ; supposeA21: m > k ; ::_thesis: contradiction A22: (Lower_Appr C) . m = Lower_Arc (L~ (Cage (C,m))) by JORDAN19:def_2; A23: Lower_Arc (L~ (Cage (C,m))) c= L~ (Cage (C,m)) by JORDAN6:61; Ball (e,r) misses L~ (Cage (C,m)) by A19, SPRECT_3:26, XBOOLE_1:63; hence contradiction by A20, A21, A22, A23, XBOOLE_1:63; ::_thesis: verum end; suppose m <= k ; ::_thesis: contradiction then LeftComp (Cage (C,m)) c= LeftComp (Cage (C,k)) by JORDAN1H:47; then A24: Ball (e,r) c= LeftComp (Cage (C,k)) by A19, XBOOLE_1:1; A25: k + 0 < k + 1 by XREAL_1:8; then LeftComp (Cage (C,k)) c= LeftComp (Cage (C,(k + 1))) by JORDAN1H:47; then Ball (e,r) c= LeftComp (Cage (C,(k + 1))) by A24, XBOOLE_1:1; then A26: Ball (e,r) misses L~ (Cage (C,(k + 1))) by SPRECT_3:26, XBOOLE_1:63; A27: Lower_Arc (L~ (Cage (C,(k + 1)))) c= L~ (Cage (C,(k + 1))) by JORDAN6:61; (Lower_Appr C) . (k + 1) = Lower_Arc (L~ (Cage (C,(k + 1)))) by JORDAN19:def_2; hence contradiction by A20, A25, A26, A27, XBOOLE_1:63; ::_thesis: verum end; end; end; end; end; end; theorem :: JORDAN22:37 for C being Simple_closed_curve holds ( ( LMP C in Lower_Arc C & UMP C in Upper_Arc C ) or ( UMP C in Lower_Arc C & LMP C in Upper_Arc C ) ) proof let C be Simple_closed_curve; ::_thesis: ( ( LMP C in Lower_Arc C & UMP C in Upper_Arc C ) or ( UMP C in Lower_Arc C & LMP C in Upper_Arc C ) ) A1: LMP C in South_Arc C by Th34; A2: North_Arc C c= C by Th35; A3: UMP C in North_Arc C by Th33; A4: South_Arc C c= C by Th36; now__::_thesis:_(_(_LE_LMP_C,_UMP_C,C_&_UMP_C_in_Lower_Arc_C_&_LMP_C_in_Upper_Arc_C_)_or_(_LE_UMP_C,_LMP_C,C_&_LMP_C_in_Lower_Arc_C_&_UMP_C_in_Upper_Arc_C_)_) percases ( LE LMP C, UMP C,C or LE UMP C, LMP C,C ) by A4, A1, A2, A3, JORDAN16:7; case LE LMP C, UMP C,C ; ::_thesis: ( UMP C in Lower_Arc C & LMP C in Upper_Arc C ) then ( ( LMP C in Upper_Arc C & UMP C in Lower_Arc C ) or ( LMP C in Lower_Arc C & UMP C in Lower_Arc C ) or ( LMP C in Upper_Arc C & UMP C in Upper_Arc C ) ) by JORDAN6:def_10; hence ( UMP C in Lower_Arc C & LMP C in Upper_Arc C ) by JORDAN21:49, JORDAN21:50; ::_thesis: verum end; case LE UMP C, LMP C,C ; ::_thesis: ( LMP C in Lower_Arc C & UMP C in Upper_Arc C ) then ( ( UMP C in Upper_Arc C & LMP C in Lower_Arc C ) or ( LMP C in Lower_Arc C & UMP C in Lower_Arc C ) or ( LMP C in Upper_Arc C & UMP C in Upper_Arc C ) ) by JORDAN6:def_10; hence ( LMP C in Lower_Arc C & UMP C in Upper_Arc C ) by JORDAN21:49, JORDAN21:50; ::_thesis: verum end; end; end; hence ( ( LMP C in Lower_Arc C & UMP C in Upper_Arc C ) or ( UMP C in Lower_Arc C & LMP C in Upper_Arc C ) ) ; ::_thesis: verum end; theorem :: JORDAN22:38 for C being Simple_closed_curve holds W-bound C = W-bound (North_Arc C) proof let C be Simple_closed_curve; ::_thesis: W-bound C = W-bound (North_Arc C) A1: W-min C in North_Arc C by Th29; North_Arc C c= C by Th35; hence W-bound C = W-bound (North_Arc C) by A1, JORDAN1J:65; ::_thesis: verum end; theorem :: JORDAN22:39 for C being Simple_closed_curve holds E-bound C = E-bound (North_Arc C) proof let C be Simple_closed_curve; ::_thesis: E-bound C = E-bound (North_Arc C) A1: E-max C in North_Arc C by Th30; North_Arc C c= C by Th35; hence E-bound C = E-bound (North_Arc C) by A1, JORDAN1J:66; ::_thesis: verum end; theorem :: JORDAN22:40 for C being Simple_closed_curve holds W-bound C = W-bound (South_Arc C) proof let C be Simple_closed_curve; ::_thesis: W-bound C = W-bound (South_Arc C) A1: W-min C in South_Arc C by Th31; South_Arc C c= C by Th36; hence W-bound C = W-bound (South_Arc C) by A1, JORDAN1J:65; ::_thesis: verum end; theorem :: JORDAN22:41 for C being Simple_closed_curve holds E-bound C = E-bound (South_Arc C) proof let C be Simple_closed_curve; ::_thesis: E-bound C = E-bound (South_Arc C) A1: E-max C in South_Arc C by Th32; South_Arc C c= C by Th36; hence E-bound C = E-bound (South_Arc C) by A1, JORDAN1J:66; ::_thesis: verum end;