:: Some Properties of Cells and Gauges :: by Adam Grabowski , Artur Korni{\l}owicz and Andrzej Trybulec :: :: Received October 13, 2000 :: Copyright (c) 2000-2016 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, TOPREAL2, SUBSET_1, PRE_TOPC, EUCLID, INT_1, ARYTM_3, ARYTM_1, CARD_1, RELAT_1, PCOMPS_1, STRUCT_0, XXREAL_0, MATRIX_1, JORDAN8, METRIC_1, MCART_1, TREES_1, FINSEQ_1, PSCOMP_1, NEWTON, GOBOARD5, TARSKI, JORDAN2C, XXREAL_2, REAL_1, COMPLEX1, XXREAL_1, XBOOLE_0, RCOMP_1, FUNCT_1, TOPREAL1, SPPOL_1, TOPS_1, SEQ_4, NAT_1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, REAL_1, RELSET_1, INT_1, XXREAL_2, SEQ_4, STRUCT_0, NAT_D, FINSEQ_1, MATRIX_0, RCOMP_1, TOPS_1, FUNCT_2, PRE_TOPC, NEWTON, COMPTS_1, EUCLID, PCOMPS_1, METRIC_1, METRIC_6, RLTOPSP1, TOPREAL1, TOPREAL2, GOBOARD5, JORDAN8, JORDAN2C, SPPOL_1, PSCOMP_1, TOPREAL6, SEQ_2; constructors REAL_1, RCOMP_1, NEWTON, TOPS_1, CONNSP_1, COMPTS_1, TBSP_1, TOPREAL2, GOBOARD1, SPPOL_1, GOBOARD5, PSCOMP_1, JORDAN2C, TOPREAL6, JORDAN8, NAT_D, SEQ_4, RELSET_1, FUNCSDOM, PCOMPS_1, SEQ_2, SQUARE_1, COMSEQ_2; registrations RELSET_1, NUMBERS, XREAL_0, NAT_1, INT_1, MEMBERED, SEQ_2, STRUCT_0, PRE_TOPC, COMPTS_1, EUCLID, TOPREAL1, TOPREAL2, PSCOMP_1, WAYBEL_2, TOPREAL5, JORDAN2C, TOPREAL6, JORDAN8, VALUED_0, SPRECT_1, NEWTON, ORDINAL1; requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM; definitions TARSKI, XBOOLE_0; equalities XBOOLE_0; expansions TARSKI, XBOOLE_0; theorems EUCLID, JORDAN8, PSCOMP_1, JORDAN1A, NAT_1, TOPREAL6, GOBOARD5, GOBRD14, JORDAN2C, GOBOARD6, TOPS_1, INT_1, TOPREAL5, JORDAN9, METRIC_1, PCOMPS_1, ABSVALUE, SPRECT_1, RELAT_1, SEQ_4, METRIC_6, TOPREAL3, UNIFORM1, JCT_MISC, FUNCT_1, XBOOLE_0, XCMPLX_1, XREAL_1, COMPLEX1, NEWTON, TOPREAL1, XXREAL_0, PRE_TOPC, MATRIX_0, XXREAL_2, NAT_D, MEASURE6; begin reserve C for Simple_closed_curve, i, j, n for Nat, p for Point of TOP-REAL 2; Lm1: now let r be Real, j; thus [\ r + j /] - j = [\ r /] + j - j by INT_1:28 .= [\ r /]; end; Lm2: for a, b, c being Real st a <> 0 & b <> 0 holds (a/b)*((c/a) * b) = c proof let a, b, c be Real; assume that A1: a <> 0 and A2: b <> 0; (a/b)*((c/a) * b) = (a/b)*b * (c/a) .= a * (c/a) by A2,XCMPLX_1:87 .= c by A1,XCMPLX_1:87; hence thesis; end; Lm3: for p being Point of TOP-REAL 2 holds p is Point of Euclid 2 proof let p be Point of TOP-REAL 2; TopSpaceMetr Euclid 2 = the TopStruct of TOP-REAL 2 by EUCLID:def 8; then the TopStruct of TOP-REAL 2 = TopStruct (#the carrier of Euclid 2, Family_open_set Euclid 2#) by PCOMPS_1:def 5; hence thesis; end; Lm4: for r being Real st r > 0 holds 2*(r/4) < r proof let r be Real; A1: 2*(r/4) = r/2; assume r > 0; hence thesis by A1,XREAL_1:216; end; theorem Th1: [i,j] in Indices Gauge(C,n) & [i+1,j] in Indices Gauge(C,n) implies dist(Gauge(C,n)*(1,1),Gauge(C,n)*(2,1)) = Gauge(C,n)*(i+1,j)`1 - Gauge( C,n)*(i,j)`1 proof set G = Gauge(C,n); assume that A1: [i,j] in Indices G and A2: [i+1,j] in Indices G; A3: j <= width G by A1,MATRIX_0:32; 1 <= j by A1,MATRIX_0:32; then A4: 1 <= width G by A3,XXREAL_0:2; A5: len G >= 4 by JORDAN8:10; then 2 <= len G by XXREAL_0:2; then A6: [2,1] in Indices G by A4,MATRIX_0:30; A7: dist(G*(i,j),G*(i+1,j)) = (E-bound C - W-bound C)/2|^n by A1,A2,GOBRD14:10; 1 <= len G by A5,XXREAL_0:2; then [1,1] in Indices G by A4,MATRIX_0:30; then dist(G*(1,1),G*(1+1,1)) = dist(G*(i,j),G*(i+1,j)) by A6,A7,GOBRD14:10 .= G*(i+1,j)`1 - G*(i,j)`1 by A1,A2,GOBRD14:5; hence thesis; end; theorem Th2: [i,j] in Indices Gauge(C,n) & [i,j+1] in Indices Gauge(C,n) implies dist(Gauge(C,n)*(1,1),Gauge(C,n)*(1,2)) = Gauge(C,n)*(i,j+1)`2 - Gauge( C,n)*(i,j)`2 proof set G = Gauge(C,n); assume that A1: [i,j] in Indices G and A2: [i,j+1] in Indices G; A3: 1 <= j+1 by A2,MATRIX_0:32; len G >= 4 by JORDAN8:10; then A4: 1 <= len G by XXREAL_0:2; 2|^n + 3 >= 3 by NAT_1:11; then width G >= 3 by JORDAN1A:28; then 2 <= width G by XXREAL_0:2; then A5: [1,2] in Indices G by A4,MATRIX_0:30; j + 1 <= width G by A2,MATRIX_0:32; then 1 <= width G by A3,XXREAL_0:2; then A6: [1,1] in Indices G by A4,MATRIX_0:30; dist(G*(i,j),G*(i,j+1)) = (N-bound C - S-bound C)/2|^n by A1,A2,GOBRD14:9; then dist(G*(1,1),G*(1,1+1)) = dist(G*(i,j),G*(i,j+1)) by A6,A5,GOBRD14:9 .= G*(i,j+1)`2 - G*(i,j)`2 by A1,A2,GOBRD14:6; hence thesis; end; TopSpaceMetr Euclid 2 = the TopStruct of TOP-REAL 2 by EUCLID:def 8; then Lm5: the TopStruct of TOP-REAL 2 = TopStruct (#the carrier of Euclid 2, Family_open_set Euclid 2#) by PCOMPS_1:def 5; Lm6: for r being Real, q being Point of Euclid 2 st 1 <= i & i+1 <= len Gauge (C,n) & 1 <= j & j+1 <= width Gauge (C,n) & r > 0 & p = q & dist(Gauge(C, n)*(1,1),Gauge(C,n)*(1,2)) < r/4 & dist(Gauge(C,n)*(1,1),Gauge(C,n)*(2,1)) < r/ 4 & p in cell (Gauge(C,n),i,j) holds cell(Gauge(C,n),i,j) c= Ball (q,r) proof let r be Real, q be Point of Euclid 2; assume that A1: 1 <= i and A2: i+1 <= len Gauge (C,n) and A3: 1 <= j and A4: j+1 <= width Gauge (C,n) and A5: r > 0 and A6: p = q and A7: dist(Gauge(C,n)*(1,1),Gauge(C,n)*(1,2)) < r/4 and A8: dist(Gauge(C,n)*(1,1),Gauge(C,n)*(2,1)) < r/4 and A9: p in cell (Gauge(C,n),i,j); set G = Gauge(C,n); set I = i, J = j, l = r/4; let x be object; assume A10: x in cell(Gauge(C,n),i,j); then reconsider Q = q, X = x as Point of TOP-REAL 2 by Lm5; A11: Q`1 <= G*(I+1,J)`1 by A1,A2,A3,A4,A6,A9,JORDAN9:17; A12: G*(I,J)`2 <= Q`2 by A1,A2,A3,A4,A6,A9,JORDAN9:17; A13: G*(I,J)`1 <= X`1 by A1,A2,A3,A4,A10,JORDAN9:17; j < j+1 by XREAL_1:29; then A14: j <= width G by A4,XXREAL_0:2; i < i + 1 by XREAL_1:29; then A15: i <= len G by A2,XXREAL_0:2; then A16: [i,j] in Indices G by A1,A3,A14,MATRIX_0:30; A17: X`2 <= G*(I,J+1)`2 by A1,A2,A3,A4,A10,JORDAN9:17; A18: G*(I,J)`2 <= X`2 by A1,A2,A3,A4,A10,JORDAN9:17; A19: Q`2 <= G*(I,J+1)`2 by A1,A2,A3,A4,A6,A9,JORDAN9:17; A20: X`1 <= G*(I+1,J)`1 by A1,A2,A3,A4,A10,JORDAN9:17; 1 <= j+1 by A3,XREAL_1:29; then [i,j+1] in Indices G by A1,A4,A15,MATRIX_0:30; then A21: G*(I,J+1)`2 - G*(I,J)`2 < l by A7,A16,Th2; 1 <= 1 + i by NAT_1:11; then [i+1,j] in Indices G by A2,A3,A14,MATRIX_0:30; then G*(I+1,J)`1 - G*(I,J)`1 < l by A8,A16,Th1; then A22: (G*(I+1,J)`1 - G*(I,J)`1 ) + ( G*(I,J+1)`2 - G*(I,J)`2 ) <= l + l by A21, XREAL_1:7; G*(I,J)`1 <= Q`1 by A1,A2,A3,A4,A6,A9,JORDAN9:17; then dist (Q,X) <= (G*(I+1,J)`1 - G*(I,J)`1 ) + ( G*(I,J+1)`2 - G*(I,J)`2 ) by A11,A12,A19,A13,A20,A18,A17,TOPREAL6:95; then A23: dist (p,X) <= l + l by A6,A22,XXREAL_0:2; reconsider x9 = x as Point of Euclid 2 by A10,Lm3; 2*(r/4) < r by A5,Lm4; then dist (X, p) < r by A23,XXREAL_0:2; then dist (x9, q) < r by A6,TOPREAL6:def 1; hence thesis by METRIC_1:11; end; theorem Th3: for S being Subset of TOP-REAL 2 st S is bounded holds proj1.:S is real-bounded proof let S be Subset of TOP-REAL 2; assume S is bounded; then reconsider C = S as bounded Subset of Euclid 2 by JORDAN2C:11; consider r being Real, x being Point of Euclid 2 such that A1: 0 < r and A2: C c= Ball(x,r) by METRIC_6:def 3; reconsider P = Ball(x,r) as Subset of TOP-REAL 2 by TOPREAL3:8; reconsider p = x as Point of TOP-REAL 2 by TOPREAL3:8; set t = max(|.p`1-r.|,|.p`1+r.|); now assume that A3: |.p`1-r.| <= 0 and A4: |.p`1+r.| <= 0; |.p`1-r.| = 0 by A3,COMPLEX1:46; then |.r-p`1.| = 0 by UNIFORM1:11; then A5: r-p`1 = 0 by ABSVALUE:2; |.p`1+r.| = 0 by A4,COMPLEX1:46; hence contradiction by A1,A5,ABSVALUE:2; end; then A6: t > 0 by XXREAL_0:30; A7: proj1.:P = ].p`1-r,p`1+r.[ by TOPREAL6:43; for s being Real st s in proj1.:S holds |.s.| < t proof let s being Real; proj1.:S c= proj1.:P by A2,RELAT_1:123; hence thesis by A7,JCT_MISC:3; end; hence thesis by A6,SEQ_4:4; end; theorem for C1 being non empty compact Subset of TOP-REAL 2, C2, S being non empty Subset of TOP-REAL 2 holds S = C1 \/ C2 & proj1.:C2 is non empty bounded_below implies W-bound S = min(W-bound C1, W-bound C2) proof let C1 be non empty compact Subset of TOP-REAL 2, C2, S be non empty Subset of TOP-REAL 2; assume that A1: S = C1 \/ C2 and A2: proj1.:C2 is non empty bounded_below; set P1 = proj1.:C1, P2 = proj1.:C2, PS = proj1.:S; A3: W-bound C1 = lower_bound P1 by SPRECT_1:43; A4: W-bound C2 = lower_bound P2 by SPRECT_1:43; thus W-bound S = lower_bound PS by SPRECT_1:43 .= lower_bound(P1 \/ P2) by A1,RELAT_1:120 .= min(W-bound C1, W-bound C2) by A2,A3,A4,SEQ_4:142; end; Lm7: for X being Subset of TOP-REAL 2 holds p in X & X is bounded implies lower_bound (proj1|X) <= p`1 & p`1 <= upper_bound (proj1|X) proof set T = TOP-REAL 2; let X be Subset of TOP-REAL 2; assume that A1: p in X and A2: X is bounded; reconsider X as non empty Subset of TOP-REAL 2 by A1; A3: the carrier of T|X = X by PRE_TOPC:8; A4: (proj1|X).:X = proj1.:X by RELAT_1:129; A5: proj1.:X is real-bounded by A2,Th3; then (proj1|X).:X is bounded_below by A4,XXREAL_2:def 11; then A6: proj1|X is bounded_below by A3,MEASURE6:def 10; (proj1|X).:X is bounded_above by A4,A5,XXREAL_2:def 11; then proj1|X is bounded_above by A3,MEASURE6:def 11; then reconsider f = proj1|X as bounded RealMap of T|X by A6; reconsider p9 = p as Point of T|X by A1,PRE_TOPC:8; A7: (proj1|X).p9 = p`1 by A1,PSCOMP_1:22; then lower_bound f <= p`1 by PSCOMP_1:1; hence thesis by A7,PSCOMP_1:4; end; Lm8: for X being Subset of TOP-REAL 2 holds p in X & X is bounded implies lower_bound (proj2|X) <= p`2 & p`2 <= upper_bound (proj2|X) proof set T = TOP-REAL 2; let X be Subset of TOP-REAL 2; assume that A1: p in X and A2: X is bounded; reconsider X as non empty Subset of TOP-REAL 2 by A1; A3: the carrier of T|X = X by PRE_TOPC:8; A4: (proj2|X).:X = proj2.:X by RELAT_1:129; A5: proj2.:X is real-bounded by A2,JCT_MISC:14; then (proj2|X).:X is bounded_below by A4,XXREAL_2:def 11; then A6: proj2|X is bounded_below by A3,MEASURE6:def 10; (proj2|X).:X is bounded_above by A4,A5,XXREAL_2:def 11; then proj2|X is bounded_above by A3,MEASURE6:def 11; then reconsider f = proj2|X as bounded RealMap of T|X by A6; reconsider p9 = p as Point of T|X by A1,PRE_TOPC:8; A7: (proj2|X).p9 = p`2 by A1,PSCOMP_1:23; then lower_bound f <= p`2 by PSCOMP_1:1; hence thesis by A7,PSCOMP_1:4; end; theorem Th5: for X being Subset of TOP-REAL 2 holds p in X & X is bounded implies W-bound X <= p`1 & p`1 <= E-bound X & S-bound X <= p`2 & p`2 <= N-bound X proof let X be Subset of TOP-REAL 2; assume that A1: p in X and A2: X is bounded; W-bound X = lower_bound (proj1|X) by PSCOMP_1:def 7; hence W-bound X <= p`1 by A1,A2,Lm7; E-bound X = upper_bound (proj1|X) by PSCOMP_1:def 9; hence E-bound X >= p`1 by A1,A2,Lm7; S-bound X = lower_bound (proj2|X) by PSCOMP_1:def 10; hence S-bound X <= p`2 by A1,A2,Lm8; N-bound X = upper_bound (proj2|X) by PSCOMP_1:def 8; hence thesis by A1,A2,Lm8; end; Lm9: for C being Subset of TOP-REAL 2 st C is bounded for h being Real st BDD C <> {} & h > W-bound BDD C & (for p st p in BDD C holds p`1 >= h) holds contradiction proof let C be Subset of TOP-REAL 2 such that A1: C is bounded; set X = proj1|BDD C; let h be Real; assume that A2: BDD C <> {} and A3: h > W-bound BDD C and A4: for p st p in BDD C holds p`1 >= h; reconsider T = (TOP-REAL 2)|BDD C as non empty TopSpace by A2; the carrier of T = BDD C by PRE_TOPC:8; then X.:the carrier of T = proj1.:BDD C by RELAT_1:129; then X.:the carrier of T is real-bounded by A1,Th3,JORDAN2C:106; then X.:the carrier of T is bounded_below by XXREAL_2:def 11; then reconsider X as bounded_below RealMap of T by MEASURE6:def 10; A5: for p being Point of T holds X.p >= h proof let p be Point of T; A6: the carrier of T = BDD C by PRE_TOPC:8; then p in BDD C; then reconsider p9 = p as Point of TOP-REAL 2; X.p = proj1.p9 by A6,FUNCT_1:49; then X.p = p9`1 by PSCOMP_1:def 5; hence thesis by A4,A6; end; lower_bound X = W-bound BDD C by PSCOMP_1:def 7; hence thesis by A3,A5,PSCOMP_1:2; end; Lm10: for C being Subset of TOP-REAL 2 st C is bounded for h being Real st BDD C <> {} & h < E-bound BDD C & (for p st p in BDD C holds p`1 <= h) holds contradiction proof let C be Subset of TOP-REAL 2 such that A1: C is bounded; set X = proj1|BDD C; let h be Real; assume that A2: BDD C <> {} and A3: h < E-bound BDD C and A4: for p st p in BDD C holds p`1 <= h; reconsider T = (TOP-REAL 2)|BDD C as non empty TopSpace by A2; the carrier of T = BDD C by PRE_TOPC:8; then X.:the carrier of T = proj1.:BDD C by RELAT_1:129; then X.:the carrier of T is real-bounded by A1,Th3,JORDAN2C:106; then X.:the carrier of T is bounded_above by XXREAL_2:def 11; then reconsider X as bounded_above RealMap of T by MEASURE6:def 11; A5: for p being Point of T holds X.p <= h proof let p be Point of T; A6: the carrier of T = BDD C by PRE_TOPC:8; then p in BDD C; then reconsider p9 = p as Point of TOP-REAL 2; X.p = proj1.p9 by A6,FUNCT_1:49; then X.p = p9`1 by PSCOMP_1:def 5; hence thesis by A4,A6; end; upper_bound X = E-bound BDD C by PSCOMP_1:def 9; hence thesis by A3,A5,PSCOMP_1:5; end; Lm11: for C being Subset of TOP-REAL 2 st C is bounded for h being Real st BDD C <> {} & h < N-bound BDD C & (for p st p in BDD C holds p`2 <= h) holds contradiction proof let C be Subset of TOP-REAL 2 such that A1: C is bounded; set X = proj2|BDD C; let h be Real; assume that A2: BDD C <> {} and A3: h < N-bound BDD C and A4: for p st p in BDD C holds p`2 <= h; reconsider T = (TOP-REAL 2)|BDD C as non empty TopSpace by A2; the carrier of T = BDD C by PRE_TOPC:8; then X.:the carrier of T = proj2.:BDD C by RELAT_1:129; then X.:the carrier of T is real-bounded by A1,JCT_MISC:14,JORDAN2C:106; then X.:the carrier of T is bounded_above by XXREAL_2:def 11; then reconsider X as bounded_above RealMap of T by MEASURE6:def 11; A5: for p being Point of T holds X.p <= h proof let p be Point of T; A6: the carrier of T = BDD C by PRE_TOPC:8; then p in BDD C; then reconsider p9 = p as Point of TOP-REAL 2; X.p = proj2.p9 by A6,FUNCT_1:49; then X.p = p9`2 by PSCOMP_1:def 6; hence thesis by A4,A6; end; upper_bound X = N-bound BDD C by PSCOMP_1:def 8; hence thesis by A3,A5,PSCOMP_1:5; end; Lm12: for C being Subset of TOP-REAL 2 st C is bounded for h being Real st BDD C <> {} & h > S-bound BDD C & (for p st p in BDD C holds p`2 >= h) holds contradiction proof let C be Subset of TOP-REAL 2 such that A1: C is bounded; set X = proj2|BDD C; let h be Real; assume that A2: BDD C <> {} and A3: h > S-bound BDD C and A4: for p st p in BDD C holds p`2 >= h; reconsider T = (TOP-REAL 2)|BDD C as non empty TopSpace by A2; the carrier of T = BDD C by PRE_TOPC:8; then X.:the carrier of T = proj2.:BDD C by RELAT_1:129; then X.:the carrier of T is real-bounded by A1,JCT_MISC:14,JORDAN2C:106; then X.:the carrier of T is bounded_below by XXREAL_2:def 11; then reconsider X as bounded_below RealMap of T by MEASURE6:def 10; A5: for p being Point of T holds X.p >= h proof let p be Point of T; A6: the carrier of T = BDD C by PRE_TOPC:8; then p in BDD C; then reconsider p9 = p as Point of TOP-REAL 2; X.p = proj2.p9 by A6,FUNCT_1:49; then X.p = p9`2 by PSCOMP_1:def 6; hence thesis by A4,A6; end; lower_bound X = S-bound BDD C by PSCOMP_1:def 10; hence thesis by A3,A5,PSCOMP_1:2; end; Lm13: now let C be Subset of TOP-REAL 2; assume C is bounded; then UBD C is_outside_component_of C by JORDAN2C:68; hence UBD C is non empty by JORDAN2C:def 3; end; theorem Th6: for C being compact Subset of TOP-REAL 2 holds BDD C <> {} implies W-bound C <= W-bound BDD C proof let C be compact Subset of TOP-REAL 2; set WC = W-bound C, WB = W-bound BDD C; set hal = (WB + WC)/2; assume that A1: BDD C <> {} and A2: WC > WB; A3: hal < WC by A2,XREAL_1:226; now per cases; suppose for q1 being Point of TOP-REAL 2 st q1 in BDD C holds q1`1 >= hal; hence contradiction by A1,A2,Lm9,XREAL_1:226; end; suppose ex q1 being Point of TOP-REAL 2 st q1 in BDD C & q1`1 < hal; then consider q1 being Point of TOP-REAL 2 such that A4: q1 in BDD C and A5: q1`1 < hal; set Q = |[(WC + q1`1)/2,q1`2]|; set WH = west_halfline Q; A6: Q`1 = (WC + q1`1)/2 by EUCLID:52; A7: q1`1 < WC by A3,A5,XXREAL_0:2; WH misses C proof A8: Q`1 < WC by A7,A6,XREAL_1:226; assume WH meets C; then consider y being object such that A9: y in WH /\ C by XBOOLE_0:4; A10: y in C by A9,XBOOLE_0:def 4; A11: y in WH by A9,XBOOLE_0:def 4; reconsider y as Point of TOP-REAL 2 by A9; y`1 <= Q`1 by A11,TOPREAL1:def 13; then y`1 < WC by A8,XXREAL_0:2; hence thesis by A10,PSCOMP_1:24; end; then A12: WH c= UBD C by JORDAN2C:126; A13: q1`2 = Q`2 by EUCLID:52; q1`1 < Q`1 by A7,A6,XREAL_1:226; then q1 in WH by A13,TOPREAL1:def 13; then q1 in BDD C /\ UBD C by A4,A12,XBOOLE_0:def 4; then BDD C meets UBD C; hence contradiction by JORDAN2C:24; end; end; hence thesis; end; theorem Th7: for C being compact Subset of TOP-REAL 2 holds BDD C <> {} implies E-bound C >= E-bound BDD C proof let C be compact Subset of TOP-REAL 2; set WC = E-bound BDD C, WB = E-bound C; set hal = (WB + WC)/2; assume that A1: BDD C <> {} and A2: WC > WB; A3: hal > WB by A2,XREAL_1:226; now per cases; suppose for q1 being Point of TOP-REAL 2 st q1 in BDD C holds q1`1 <= hal; hence contradiction by A1,A2,Lm10,XREAL_1:226; end; suppose ex q1 being Point of TOP-REAL 2 st q1 in BDD C & q1`1 > hal; then consider q1 being Point of TOP-REAL 2 such that A4: q1 in BDD C and A5: q1`1 > hal; set Q = |[(WB + q1`1)/2,q1`2]|; set WH = east_halfline Q; A6: Q`1 = (WB + q1`1)/2 by EUCLID:52; A7: q1`1 > WB by A3,A5,XXREAL_0:2; WH misses C proof A8: Q`1 > WB by A7,A6,XREAL_1:226; assume WH /\ C <> {}; then consider y being object such that A9: y in WH /\ C by XBOOLE_0:def 1; A10: y in C by A9,XBOOLE_0:def 4; A11: y in WH by A9,XBOOLE_0:def 4; reconsider y as Point of TOP-REAL 2 by A9; y`1 >= Q`1 by A11,TOPREAL1:def 11; then y`1 > WB by A8,XXREAL_0:2; hence thesis by A10,PSCOMP_1:24; end; then A12: WH c= UBD C by JORDAN2C:127; A13: q1`2 = Q`2 by EUCLID:52; q1`1 > Q`1 by A7,A6,XREAL_1:226; then q1 in WH by A13,TOPREAL1:def 11; then q1 in BDD C /\ UBD C by A4,A12,XBOOLE_0:def 4; then BDD C meets UBD C; hence contradiction by JORDAN2C:24; end; end; hence thesis; end; theorem Th8: for C being compact Subset of TOP-REAL 2 holds BDD C <> {} implies S-bound C <= S-bound BDD C proof let C be compact Subset of TOP-REAL 2; set WC = S-bound C, WB = S-bound BDD C; set hal = (WB + WC)/2; assume that A1: BDD C <> {} and A2: WC > WB; A3: hal < WC by A2,XREAL_1:226; now per cases; suppose for q1 being Point of TOP-REAL 2 st q1 in BDD C holds q1`2 >= hal; hence contradiction by A1,A2,Lm12,XREAL_1:226; end; suppose ex q1 being Point of TOP-REAL 2 st q1 in BDD C & q1`2 < hal; then consider q1 being Point of TOP-REAL 2 such that A4: q1 in BDD C and A5: q1`2 < hal; set Q = |[q1`1,(WC + q1`2)/2]|; set WH = south_halfline Q; A6: Q`2 = (WC + q1`2)/2 by EUCLID:52; A7: q1`2 < WC by A3,A5,XXREAL_0:2; WH misses C proof A8: Q`2 < WC by A7,A6,XREAL_1:226; assume WH /\ C <> {}; then consider y being object such that A9: y in WH /\ C by XBOOLE_0:def 1; A10: y in C by A9,XBOOLE_0:def 4; A11: y in WH by A9,XBOOLE_0:def 4; reconsider y as Point of TOP-REAL 2 by A9; y`2 <= Q`2 by A11,TOPREAL1:def 12; then y`2 < WC by A8,XXREAL_0:2; hence thesis by A10,PSCOMP_1:24; end; then A12: WH c= UBD C by JORDAN2C:128; A13: q1`1 = Q`1 by EUCLID:52; q1`2 < Q`2 by A7,A6,XREAL_1:226; then q1 in WH by A13,TOPREAL1:def 12; then q1 in BDD C /\ UBD C by A4,A12,XBOOLE_0:def 4; then BDD C meets UBD C; hence contradiction by JORDAN2C:24; end; end; hence thesis; end; theorem Th9: for C being compact Subset of TOP-REAL 2 holds BDD C <> {} implies N-bound C >= N-bound BDD C proof let C be compact Subset of TOP-REAL 2; set WC = N-bound BDD C, WB = N-bound C; set hal = (WB + WC)/2; assume that A1: BDD C <> {} and A2: WC > WB; A3: hal > WB by A2,XREAL_1:226; now per cases; suppose for q1 being Point of TOP-REAL 2 st q1 in BDD C holds q1`2 <= hal; hence contradiction by A1,A2,Lm11,XREAL_1:226; end; suppose ex q1 being Point of TOP-REAL 2 st q1 in BDD C & q1`2 > hal; then consider q1 being Point of TOP-REAL 2 such that A4: q1 in BDD C and A5: q1`2 > hal; set Q = |[q1`1,(WB + q1`2)/2]|; set WH = north_halfline Q; A6: Q`2 = (WB + q1`2)/2 by EUCLID:52; A7: q1`2 > WB by A3,A5,XXREAL_0:2; WH misses C proof A8: Q`2 > WB by A7,A6,XREAL_1:226; assume WH /\ C <> {}; then consider y being object such that A9: y in WH /\ C by XBOOLE_0:def 1; A10: y in C by A9,XBOOLE_0:def 4; A11: y in WH by A9,XBOOLE_0:def 4; reconsider y as Point of TOP-REAL 2 by A9; y`2 >= Q`2 by A11,TOPREAL1:def 10; then y`2 > WB by A8,XXREAL_0:2; hence thesis by A10,PSCOMP_1:24; end; then A12: WH c= UBD C by JORDAN2C:129; A13: q1`1 = Q`1 by EUCLID:52; q1`2 > Q`2 by A7,A6,XREAL_1:226; then q1 in WH by A13,TOPREAL1:def 10; then q1 in BDD C /\ UBD C by A4,A12,XBOOLE_0:def 4; then BDD C meets UBD C; hence contradiction by JORDAN2C:24; end; end; hence thesis; end; theorem Th10: for C being compact non vertical Subset of TOP-REAL 2 for I being Integer st p in BDD C & I = [\ ((p`1 - W-bound C) / (E-bound C - W-bound C) * 2|^n) + 2 /] holds 1 < I proof let C be compact non vertical Subset of TOP-REAL 2; set W = W-bound C, E = E-bound C; set pW = p`1 - W, EW = E - W; let I be Integer; assume that A1: p in BDD C and A2: I = [\ (pW / EW * 2|^n) + 2 /]; A3: W <= W-bound BDD C by A1,Th6; BDD C is bounded by JORDAN2C:106; then p`1 >= W-bound BDD C by A1,Th5; then p`1 >= W by A3,XXREAL_0:2; then A4: pW >= 0 by XREAL_1:48; set K = [\ pW / EW * 2|^n /]; pW / EW * 2|^n - 1 < K by INT_1:def 6; then A5: pW / EW * 2|^n - 1 + 2 < K + 2 by XREAL_1:6; EW > 0 by SPRECT_1:31,XREAL_1:50; then pW / EW * 2|^n + 1 >= 0 + 1 by A4,XREAL_1:6; then 1 < K + 2 by A5,XXREAL_0:2; hence thesis by A2,INT_1:28; end; theorem Th11: for C being compact non vertical Subset of TOP-REAL 2 for I being Integer st p in BDD C & I = [\ ((p`1 - W-bound C) / (E-bound C - W-bound C) * 2|^n) + 2 /] holds I + 1 <= len Gauge (C, n) proof let C be compact non vertical Subset of TOP-REAL 2; set W = W-bound C, E = E-bound C; set EW = E-W, pW = p`1 - W; let I be Integer; assume that A1: p in BDD C and A2: I = [\ (pW / EW * 2|^n) + 2 /]; A3: E >= E-bound BDD C by A1,Th7; BDD C is bounded by JORDAN2C:106; then p`1 <= E-bound BDD C by A1,Th5; then p`1 <= E by A3,XXREAL_0:2; then A4: p`1 - W <= EW by XREAL_1:9; EW > 0 by SPRECT_1:31,XREAL_1:50; then pW / EW <= 1 by A4,XREAL_1:185; then pW / EW * 2|^n <= 1 * 2|^n by XREAL_1:64; then A5: pW / EW * 2|^n + 3 <= 2|^n + 3 by XREAL_1:7; I <= (pW / EW * 2|^n) + 2 by A2,INT_1:def 6; then A6: I + 1 <= (pW / EW * 2|^n) + 2 + 1 by XREAL_1:6; len Gauge (C, n) = 2|^n + 3 by JORDAN8:def 1; hence thesis by A5,A6,XXREAL_0:2; end; theorem Th12: for C being compact non horizontal Subset of TOP-REAL 2 for J being Integer st p in BDD C & J = [\ ((p`2 - S-bound C) / (N-bound C - S-bound C) * 2|^n) + 2 /] holds 1 < J & J+1 <= width Gauge (C, n) proof let C be compact non horizontal Subset of TOP-REAL 2; set W = S-bound C, E = N-bound C; set EW = E-W, pW = p`2 - W; let I be Integer; assume that A1: p in BDD C and A2: I = [\ (pW / EW * 2|^n) + 2 /]; A3: EW > 0 by SPRECT_1:32,XREAL_1:50; set K = [\ pW / EW * 2|^n /]; pW / EW * 2|^n - 1 < K by INT_1:def 6; then A4: pW / EW * 2|^n - 1 + 2 < K + 2 by XREAL_1:6; A5: W <= S-bound BDD C by A1,Th8; BDD C is bounded by JORDAN2C:106; then p`2 >= S-bound BDD C by A1,Th5; then p`2 >= W by A5,XXREAL_0:2; then pW >= 0 by XREAL_1:48; then pW / EW * 2|^n + 1 >= 0 + 1 by A3,XREAL_1:6; then 1 < K + 2 by A4,XXREAL_0:2; hence 1 < I by A2,INT_1:28; A6: len Gauge (C, n) = width Gauge (C, n) by JORDAN8:def 1; A7: E >= N-bound BDD C by A1,Th9; BDD C is bounded by JORDAN2C:106; then p`2 <= N-bound BDD C by A1,Th5; then p`2 <= E by A7,XXREAL_0:2; then p`2 - W <= EW by XREAL_1:9; then pW / EW <= 1 by A3,XREAL_1:185; then pW / EW * 2|^n <= 1 * 2|^n by XREAL_1:64; then A8: pW / EW * 2|^n + 3 <= 2|^n + 3 by XREAL_1:7; I <= (pW / EW * 2|^n) + 2 by A2,INT_1:def 6; then A9: I + 1 <= (pW / EW * 2|^n) + 2 + 1 by XREAL_1:6; len Gauge (C, n) = 2|^n + 3 by JORDAN8:def 1; hence thesis by A6,A8,A9,XXREAL_0:2; end; theorem Th13: for I being Integer st I = [\ ((p`1 - W-bound C) / (E-bound C - W-bound C) * 2|^n) + 2 /] holds (W-bound C) + (((E-bound C)-(W-bound C))/(2|^n) )*(I-2) <= p`1 proof set W = W-bound C, EW = E-bound C - W-bound C; set PW = p`1 - W; set KI = [\ (PW / EW * 2|^n) /]; let I be Integer; A1: EW > 0 by TOPREAL5:17,XREAL_1:50; 2|^n > 0 by NEWTON:83; then A2: (EW/(2|^n))*(PW / EW * 2|^n) = PW by A1,Lm2; assume I = [\ (PW / EW * 2|^n) + 2 /]; then A3: I - 2 = [\ (PW / EW * 2|^n) /] by Lm1; KI <= PW / EW * 2|^n by INT_1:def 6; then A4: (EW/(2|^n))*KI <= (EW/(2|^n))*(PW / EW * 2|^n) by A1,XREAL_1:64; W + PW = p`1; hence thesis by A3,A2,A4,XREAL_1:6; end; theorem Th14: for I being Integer st I = [\ ((p`1 - W-bound C) / (E-bound C - W-bound C) * 2|^n) + 2 /] holds p`1 < (W-bound C) + (((E-bound C)-(W-bound C))/ (2|^n))*(I-1) proof set W = W-bound C, E = E-bound C; set EW = E - W, PW = p`1 - W; let I be Integer; set KI = I - 1; A1: 2|^n > 0 by NEWTON:83; assume I = [\ (PW / EW * 2|^n) + 2 /]; then I > (PW / EW * 2|^n) + 2 - 1 by INT_1:def 6; then A2: I - 1 > (PW / EW * 2|^n) + 1 - 1 by XREAL_1:9; A3: EW > 0 by TOPREAL5:17,XREAL_1:50; then EW/(2|^n) > 0 by A1,XREAL_1:139; then A4: (EW/(2|^n))*KI > (EW/(2|^n))*(PW / EW * 2|^n) by A2,XREAL_1:68; A5: W + PW = p`1; (EW/(2|^n))*(PW / EW * 2|^n) = PW by A3,A1,Lm2; hence thesis by A5,A4,XREAL_1:6; end; theorem Th15: for J being Integer st J = [\ ((p`2 - S-bound C) / (N-bound C - S-bound C) * 2|^n) + 2 /] holds (S-bound C) + ((N-bound C - S-bound C)/(2|^n))* (J-2) <= p`2 proof set W = S-bound C, EW = N-bound C - S-bound C; set PW = p`2 - W; set KI = [\ (PW / EW * 2|^n) /]; let I be Integer; A1: EW > 0 by TOPREAL5:16,XREAL_1:50; 2|^n > 0 by NEWTON:83; then A2: (EW/(2|^n))*(PW / EW * 2|^n) = PW by A1,Lm2; assume I = [\ (PW / EW * 2|^n) + 2 /]; then A3: I - 2 = [\ (PW / EW * 2|^n) /] by Lm1; KI <= PW / EW * 2|^n by INT_1:def 6; then A4: (EW/(2|^n))*KI <= (EW/(2|^n))*(PW / EW * 2|^n) by A1,XREAL_1:64; W + PW = p`2; hence thesis by A3,A2,A4,XREAL_1:6; end; theorem Th16: for J being Integer st J = [\ ((p`2 - S-bound C) / (N-bound C - S-bound C) * 2|^n) + 2 /] holds p`2 < (S-bound C) + ((N-bound C - S-bound C)/(2 |^n))*(J-1) proof set W = S-bound C, E = N-bound C; set EW = E - W, PW = p`2 - W; let I be Integer; set KI = I - 1; A1: 2|^n > 0 by NEWTON:83; assume I = [\ (PW / EW * 2|^n) + 2 /]; then I > (PW / EW * 2|^n) + 2 - 1 by INT_1:def 6; then A2: I - 1 > (PW / EW * 2|^n) + 1 - 1 by XREAL_1:9; A3: W + PW = p`2; A4: EW > 0 by TOPREAL5:16,XREAL_1:50; then A5: EW/(2|^n) > 0 by A1,XREAL_1:139; (EW/(2|^n)) * (PW / EW * 2|^n) = PW by A4,A1,Lm2; then (EW/(2|^n))*KI > PW by A2,A5,XREAL_1:68; hence thesis by A3,XREAL_1:6; end; theorem Th17: for C being closed Subset of TOP-REAL 2, p being Point of Euclid 2 st p in BDD C ex r being Real st r > 0 & Ball(p,r) c= BDD C proof let C be closed Subset of TOP-REAL 2, p be Point of Euclid 2; set W = Int BDD C; assume p in BDD C; then p in W by TOPS_1:23; then consider r being Real such that A1: r > 0 and A2: Ball(p,r) c= BDD C by GOBOARD6:5; reconsider r as Real; take r; thus thesis by A1,A2; end; theorem for p, q being Point of TOP-REAL 2, r being Real st dist(Gauge( C,n)*(1,1),Gauge(C,n)*(1,2)) < r & dist(Gauge(C,n)*(1,1),Gauge(C,n)*(2,1)) < r & p in cell (Gauge (C, n), i, j) & q in cell (Gauge (C, n), i, j) & 1 <= i & i+ 1 <= len Gauge (C,n) & 1 <= j & j+1 <= width Gauge(C,n) holds dist (p,q) < 2 * r proof set G = Gauge (C, n); let p, q be Point of TOP-REAL 2, r be Real; assume that A1: dist(G*(1,1),G*(1,2)) < r and A2: dist(G*(1,1),G*(2,1)) < r and A3: p in cell (G, i, j) and A4: q in cell (G, i, j) and A5: 1 <= i and A6: i+1 <= len G and A7: 1 <= j and A8: j+1 <= width G; A9: p`1 <= G*(i+1,j)`1 by A3,A5,A6,A7,A8,JORDAN9:17; A10: p`2 <= G*(i,j+1)`2 by A3,A5,A6,A7,A8,JORDAN9:17; A11: G*(i,j)`2 <= p`2 by A3,A5,A6,A7,A8,JORDAN9:17; j <= j+1 by NAT_1:11; then A12: j <= width G by A8,XXREAL_0:2; i <= i+1 by NAT_1:11; then A13: i <= len G by A6,XXREAL_0:2; then A14: [i,j] in Indices G by A5,A7,A12,MATRIX_0:30; A15: q`2 <= G*(i,j+1)`2 by A4,A5,A6,A7,A8,JORDAN9:17; A16: G*(i,j)`2 <= q`2 by A4,A5,A6,A7,A8,JORDAN9:17; A17: q`1 <= G*(i+1,j)`1 by A4,A5,A6,A7,A8,JORDAN9:17; A18: G*(i,j)`1 <= q`1 by A4,A5,A6,A7,A8,JORDAN9:17; 1 <= j+1 by NAT_1:11; then [i,j+1] in Indices G by A5,A8,A13,MATRIX_0:30; then A19: G*(i,j+1)`2 - G*(i,j)`2 < r by A1,A14,Th2; 1 <= i+1 by NAT_1:11; then [i+1,j] in Indices G by A6,A7,A12,MATRIX_0:30; then G*(i+1,j)`1 - G*(i,j)`1 < r by A2,A14,Th1; then A20: (G*(i+1,j)`1 - G*(i,j)`1 ) + ( G*(i,j+1)`2 - G*(i,j)`2 ) < r + r by A19, XREAL_1:8; G*(i,j)`1 <= p`1 by A3,A5,A6,A7,A8,JORDAN9:17; then dist (p,q) <= (G*(i+1,j)`1 - G*(i,j)`1 ) + ( G*(i,j+1)`2 - G*(i,j)`2 ) by A9,A11,A10,A18,A17,A16,A15,TOPREAL6:95; hence thesis by A20,XXREAL_0:2; end; theorem for C being compact Subset of TOP-REAL 2 holds p in BDD C implies p`2 <> N-bound BDD C proof reconsider P = p as Point of Euclid 2 by Lm3; let C be compact Subset of TOP-REAL 2; A1: BDD C is bounded by JORDAN2C:106; assume p in BDD C; then consider r being Real such that A2: r > 0 and A3: Ball(P,r) c= BDD C by Th17; set EX = |[p`1, p`2 + r/2]|; 0 < r/2 by A2,XREAL_1:139; then A4: p`2 + r/2 > p`2 + 0 by XREAL_1:6; assume A5: p`2 = N-bound BDD C; A6: not EX in BDD C proof assume EX in BDD C; then EX`2 <= N-bound BDD C by A1,Th5; hence thesis by A5,A4,EUCLID:52; end; A7: P = |[p`1,p`2]| by EUCLID:53; r/2 < r by A2,XREAL_1:216; then EX in Ball(P,r) by A2,A7,GOBOARD6:8; hence thesis by A3,A6; end; theorem for C being compact Subset of TOP-REAL 2 holds p in BDD C implies p`1 <> E-bound BDD C proof reconsider P = p as Point of Euclid 2 by Lm3; let C be compact Subset of TOP-REAL 2; A1: BDD C is bounded by JORDAN2C:106; assume p in BDD C; then consider r being Real such that A2: r > 0 and A3: Ball(P,r) c= BDD C by Th17; set EX = |[p`1 + r/2, p`2]|; 0 < r/2 by A2,XREAL_1:139; then A4: p`1 + r/2 > p`1 + 0 by XREAL_1:6; assume A5: p`1 = E-bound BDD C; A6: not EX in BDD C proof assume EX in BDD C; then EX`1 <= E-bound BDD C by A1,Th5; hence thesis by A5,A4,EUCLID:52; end; A7: P = |[p`1,p`2]| by EUCLID:53; r/2 < r by A2,XREAL_1:216; then EX in Ball(P,r) by A2,A7,GOBOARD6:7; hence thesis by A3,A6; end; theorem for C being compact Subset of TOP-REAL 2 holds p in BDD C implies p`2 <> S-bound BDD C proof reconsider P = p as Point of Euclid 2 by Lm3; let C be compact Subset of TOP-REAL 2; A1: BDD C is bounded by JORDAN2C:106; assume p in BDD C; then consider r being Real such that A2: r > 0 and A3: Ball(P,r) c= BDD C by Th17; set EX = |[p`1, p`2 - r/2]|; 0 < r/2 by A2,XREAL_1:139; then p`2 + r/2 > p`2 + 0 by XREAL_1:6; then A4: p`2 - r/2 < p`2 by XREAL_1:19; assume A5: p`2 = S-bound BDD C; A6: not EX in BDD C proof assume EX in BDD C; then EX`2 >= S-bound BDD C by A1,Th5; hence thesis by A5,A4,EUCLID:52; end; A7: P = |[p`1,p`2]| by EUCLID:53; r/2 < r by A2,XREAL_1:216; then EX in Ball(P,r) by A2,A7,GOBOARD6:10; hence thesis by A3,A6; end; theorem Th22: for C being compact Subset of TOP-REAL 2 holds p in BDD C implies p`1 <> W-bound BDD C proof reconsider P = p as Point of Euclid 2 by Lm3; let C be compact Subset of TOP-REAL 2; A1: BDD C is bounded by JORDAN2C:106; assume p in BDD C; then consider r being Real such that A2: r > 0 and A3: Ball(P,r) c= BDD C by Th17; set EX = |[p`1 - r/2, p`2]|; 0 < r/2 by A2,XREAL_1:139; then p`1 + r/2 > p`1 + 0 by XREAL_1:6; then A4: p`1 - r/2 < p`1 by XREAL_1:19; assume A5: p`1 = W-bound BDD C; A6: not EX in BDD C proof assume EX in BDD C; then EX`1 >= W-bound BDD C by A1,Th5; hence thesis by A5,A4,EUCLID:52; end; A7: P = |[p`1,p`2]| by EUCLID:53; r/2 < r by A2,XREAL_1:216; then EX in Ball(P,r) by A2,A7,GOBOARD6:9; hence thesis by A3,A6; end; theorem p in BDD C implies ex n,i,j being Nat st 1 < i & i < len Gauge(C,n) & 1 < j & j < width Gauge(C,n) & p`1 <> (Gauge(C,n)*(i,j))`1 & p in cell(Gauge(C,n),i,j) & cell(Gauge(C,n),i,j) c= BDD C proof reconsider P = p as Point of Euclid 2 by Lm3; set W = W-bound C, E = E-bound C, S = S-bound C, N = N-bound C; set EW = E-W, NS = N-S; assume A1: p in BDD C; then consider r being Real such that A2: r > 0 and A3: Ball(P,r) c= BDD C by Th17; set l = r/4; l > 0 by A2,XREAL_1:139; then consider n being Nat such that 1 < n and A4: dist(Gauge(C,n)*(1,1),Gauge(C,n)*(1,2)) < l and A5: dist(Gauge(C,n)*(1,1),Gauge(C,n)*(2,1)) < l by GOBRD14:11; set I = [\ ((p`1 - W) / EW * 2|^n) + 2 /], J = [\ ((p`2 - S) / NS * 2|^n) + 2 /]; A6: 1 < J by A1,Th12; set G = Gauge(C,n); A7: I+1 <= len G by A1,Th11; A8: J+1 <= width G by A1,Th12; take n; A9: 1 < I by A1,Th10; then reconsider I, J as Element of NAT by A6,INT_1:3; A10: I < I + 1 by XREAL_1:29; then A11: I <= len G by A7,XXREAL_0:2; 1 <= J + 1 by NAT_1:11; then [I,J+1] in Indices G by A9,A8,A11,MATRIX_0:30; then G*(I,J+1) = |[W+(EW/(2|^n))*(I-2), S+(NS/(2|^n))*(J+1-2)]| by JORDAN8:def 1; then A12: G*(I,J+1)`2 = S+(NS/(2|^n))*(J-1) by EUCLID:52; then A13: p`2 < G*(I,J+1)`2 by Th16; A14: J < J + 1 by XREAL_1:29; then A15: J <= width G by A8,XXREAL_0:2; then [I,J] in Indices G by A9,A6,A11,MATRIX_0:30; then A16: G*(I,J) = |[W+(EW/(2|^n))*(I-2), S+(NS/(2|^n))*(J-2)]| by JORDAN8:def 1; then G*(I,J)`1 = W+(EW/(2|^n))*(I-2) by EUCLID:52; then A17: G*(I,J)`1 <= p`1 by Th13; 1 <= I + 1 by NAT_1:11; then [I+1,J] in Indices G by A7,A6,A15,MATRIX_0:30; then G*(I+1,J) = |[W+(EW/(2|^n))*(I+1-2), S+(NS/(2|^n))*(J-2)]| by JORDAN8:def 1; then G*(I+1,J)`1 = W+(EW/(2|^n))*(I-1) by EUCLID:52; then A18: p`1 < G*(I+1,J)`1 by Th14; G*(I,J)`2 = S+(NS/(2|^n))*(J-2) by A16,EUCLID:52; then A19: G*(I,J)`2 <= p`2 by Th15; A20: S + (NS/(2|^n))*(J-1) > p`2 by Th16; then A21: p in cell(G,I,J) by A9,A7,A6,A8,A17,A19,A18,A12,JORDAN9:17; per cases; suppose A22: p`1 <> G*(I,J)`1; take I, J; thus 1 < I & I < len G & 1 < J & J < width G by A1,A7,A8,A10,A14,Th10,Th12, XXREAL_0:2; cell(G,I,J) c= Ball(P,r) by A2,A4,A5,A9,A7,A6,A8,A21,Lm6; hence thesis by A3,A9,A7,A6,A8,A20,A17,A19,A18,A12,A22,JORDAN9:17; end; suppose A23: p`1 = G*(I,J)`1; then A24: p`1 <= G*(I-'1+1,J)`1 by A9,XREAL_1:235; A25: I-'1+1 <= len G by A9,A11,XREAL_1:235; A26: 1 <= J by A1,Th12; A27: 1 <= I-'1 by A1,Th10,NAT_D:49; then I-'1 < I by NAT_D:51; then A28: p`1 > G*(I-'1,J)`1 by A11,A15,A23,A27,A26,GOBOARD5:3; take I-'1, J; A29: J + 1 <= width G by A1,Th12; A30: 1 <= I-'1 by A1,Th10,NAT_D:49; then A31: I-'1 < I by NAT_D:51; len G = width G by JORDAN8:def 1; then A32: J <= len G by A8,A14,XXREAL_0:2; I-'1 <> 1 proof assume I-'1 = 1; then 1 = I - 1 by NAT_D:39; then G*(I,J)`1 = W-bound C by A6,A32,JORDAN8:11; then p`1 <= W-bound BDD C by A1,A23,Th6; then A33: p`1 < W-bound BDD C by A1,Th22,XXREAL_0:1; BDD C is bounded by JORDAN2C:106; hence thesis by A1,A33,Th5; end; hence 1 < I-'1 & I-'1 < len G & 1 < J & J < width G by A1,A14,A11,A30,A29 ,A31,Th12,XXREAL_0:1,2; A34: I-'1+1 <= len G by A9,A11,XREAL_1:235; A35: J + 1 <= width G by A1,Th12; A36: p`1 <= G*(I-'1+1,J)`1 by A9,A23,XREAL_1:235; A37: 1 <= J by A1,Th12; A38: I-'1+1 = I by A9,XREAL_1:235; then A39: G*(I-'1,J)`2 = G*(I,J)`2 by A11,A30,A37,A29,JORDAN9:16; A40: G*(I-'1,J+1)`2 = G*(I,J+1)`2 by A11,A38,A30,A37,A29,JORDAN9:16; p`1 > G*(I-'1,J)`1 by A11,A15,A23,A30,A37,A31,GOBOARD5:3; then p in cell (G,I-'1,J) by A19,A13,A30,A34,A37,A29,A36,A39,A40,JORDAN9:17 ; then cell(G,I-'1,J) c= Ball(P,r) by A2,A4,A5,A27,A25,A26,A35,Lm6; hence thesis by A3,A19,A13,A39,A40,A27,A25,A26,A35,A24,A28,JORDAN9:17; end; end; theorem for C being Subset of TOP-REAL 2 st C is bounded holds UBD C is non empty by Lm13;