:: Properties of Left-, and Right Components :: by Artur Korni{\l}owicz :: :: Received May 5, 1999 :: Copyright (c) 1999-2018 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, SUBSET_1, FUNCT_1, GOBOARD5, SPRECT_2, PRE_TOPC, EUCLID, RCOMP_1, SPPOL_1, GOBOARD1, STRUCT_0, JORDAN2C, TOPREAL1, REAL_1, XXREAL_0, CARD_1, METRIC_1, TARSKI, XXREAL_2, ARYTM_3, XBOOLE_0, COMPLEX1, RELAT_2, CONNSP_1, FINSEQ_1, TREES_1, CARD_3, FUNCOP_1, XXREAL_1, RELAT_1, MCART_1, MATRIX_1, ARYTM_1, SQUARE_1, JORDAN8, NEWTON, PSCOMP_1, INT_1, POWER, GOBOARD9, RLTOPSP1, GOBOARD2, PARTFUN1, TOPS_1, JORDAN1, FINSEQ_6, SPRECT_1, SEQ_4, FINSEQ_2, NAT_1; notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, BINOP_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, XXREAL_0, XXREAL_2, SQUARE_1, NAT_1, INT_1, INT_2, NEWTON, POWER, MATRIX_0, NAT_D, MATRIX_1, FUNCT_4, SEQ_4, METRIC_1, TBSP_1, FINSEQ_1, CARD_3, FINSEQ_2, FINSEQ_6, STRUCT_0, RCOMP_1, PRE_TOPC, TOPS_1, CONNSP_1, COMPTS_1, RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD2, GOBOARD5, GOBOARD9, PSCOMP_1, SPPOL_1, SPRECT_1, SPRECT_2, JORDAN2C, JORDAN8, TOPREAL6; constructors FUNCT_4, REAL_1, SQUARE_1, RCOMP_1, NEWTON, POWER, NAT_D, TOPS_1, CONNSP_1, COMPTS_1, TBSP_1, MONOID_0, TOPREAL4, GOBOARD2, SPPOL_1, JORDAN1, PSCOMP_1, GOBOARD9, SPRECT_1, SPRECT_2, JORDAN2C, TOPREAL6, JORDAN8, GOBOARD1, SEQ_4, RELSET_1, CONVEX1, BINOP_2, MATRIX_1, BINOP_1; registrations SUBSET_1, NUMBERS, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_6, STRUCT_0, PRE_TOPC, TOPS_1, MONOID_0, EUCLID, GOBOARD2, GOBRD11, SPRECT_1, SPRECT_3, JORDAN2C, REVROT_1, TOPREAL6, FUNCT_1, FINSEQ_1, PSCOMP_1, RELSET_1, JORDAN5A, NEWTON, SQUARE_1, ORDINAL1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions TARSKI, JORDAN2C, SPRECT_1, XBOOLE_0; equalities JORDAN2C, XBOOLE_0, SQUARE_1, SUBSET_1, EUCLID; expansions TARSKI, JORDAN2C, XBOOLE_0; theorems ABSVALUE, CARD_3, FUNCT_4, COMPTS_1, CONNSP_1, EUCLID, FINSEQ_1, FUNCT_1, FUNCT_2, GOBOARD5, GOBOARD6, GOBOARD7, GOBOARD9, GOBRD11, GOBRD12, INT_1, JORDAN2C, JORDAN8, METRIC_1, NAT_1, POWER, PRE_TOPC, PRE_FF, PSCOMP_1, RCOMP_1, RELAT_1, SEQ_4, SPRECT_1, SPRECT_3, SPRECT_4, SQUARE_1, SPPOL_2, SUBSET_1, TARSKI, TBSP_1, TDLAT_1, TOPREAL1, TOPREAL3, TOPREAL6, TOPS_1, SPRECT_2, REVROT_1, FINSEQ_6, XBOOLE_0, XBOOLE_1, XREAL_0, XCMPLX_1, COMPLEX1, XREAL_1, NEWTON, XXREAL_0, FINSEQ_2, MATRIX_0, XXREAL_1, NAT_D, RLTOPSP1; begin :: Components reserve i, j, n for Nat, f for non constant standard special_circular_sequence, g for clockwise_oriented non constant standard special_circular_sequence, p, q for Point of TOP-REAL 2, P for Subset of TOP-REAL 2, C for compact non vertical non horizontal Subset of TOP-REAL 2, G for Go-board; Lm1: the carrier of TOP-REAL 2 = REAL 2 by EUCLID:22; theorem for p being Point of Euclid 2 st p = 0.REAL 2 & P is_outside_component_of L~f ex r being Real st r > 0 & Ball(p,r)` c= P proof let p be Point of Euclid 2 such that A1: p = 0.REAL 2 and A2: P is_outside_component_of L~f; reconsider D = L~f as bounded Subset of Euclid 2 by JORDAN2C:11; consider r being Real, c being Point of Euclid 2 such that A3: 0 < r and c in D and A4: for z being Point of Euclid 2 st z in D holds dist(c,z) <= r by TBSP_1:10; set rr = dist(p,c)+r+1; take rr; set L = (REAL 2) \ {a where a is Point of TOP-REAL 2: |.a.| < rr}; dist(p,c)+r+0 < rr by XREAL_1:8; hence 0 < rr by A3,METRIC_1:5,XREAL_1:8; then rr = |.rr.| by ABSVALUE:def 1; then for a being Point of TOP-REAL 2 holds a <> |[0,rr]| or |.a.| >= rr by TOPREAL6:23; then not |[0,rr]| in {a where a is Point of TOP-REAL 2: |.a.| < rr}; then reconsider L as non empty Subset of TOP-REAL 2 by Lm1,XBOOLE_0:def 5; let x be object; assume A5: x in Ball(p,rr)`; then reconsider y = x as Point of Euclid 2; reconsider z = y as Point of TOP-REAL 2 by EUCLID:22; A6: dist(p,y) = |.z.| by A1,TOPREAL6:25; A7: D c= Ball(p,rr) proof let x be object; A8: dist(p,c) + r + 0 < dist(p,c) + r + 1 by XREAL_1:6; assume A9: x in D; then reconsider z = x as Point of Euclid 2; dist(c,z) <= r by A4,A9; then A10: dist(p,c) + dist(c,z) <= dist(p,c) + r by XREAL_1:7; dist(p,z) <= dist(p,c) + dist(c,z) by METRIC_1:4; then dist(p,z) <= dist(p,c) + r by A10,XXREAL_0:2; then dist(p,z) < dist(p,c) + r + 1 by A8,XXREAL_0:2; hence thesis by METRIC_1:11; end; A11: L c= (L~f)` proof let l be object; assume A12: l in L; then reconsider j = l as Point of TOP-REAL 2; reconsider t = j as Point of Euclid 2 by EUCLID:22; not l in {a where a is Point of TOP-REAL 2: |.a.| < rr} by A12, XBOOLE_0:def 5; then A13: |.j.| >= rr; now assume l in L~f; then dist(t,p) < rr by A7,METRIC_1:11; hence contradiction by A1,A13,TOPREAL6:25; end; hence thesis by A12,SUBSET_1:29; end; L is connected by JORDAN2C:53; then consider M being Subset of TOP-REAL 2 such that A14: M is_a_component_of (L~f)` and A15: L c= M by A11,GOBOARD9:3; M is_outside_component_of L~f proof reconsider W = L as Subset of Euclid 2; thus M is_a_component_of (L~f)` by A14; W is not bounded by JORDAN2C:62; then L is not bounded by JORDAN2C:11; hence thesis by A15,RLTOPSP1:42; end; then A16: M in {W where W is Subset of TOP-REAL 2: W is_outside_component_of L~ f }; not x in Ball(p,rr) by A5,XBOOLE_0:def 5; then for k being Point of TOP-REAL 2 holds k <> z or |.k.| >= rr by A6, METRIC_1:11; then z in REAL 2 & not x in {a where a is Point of TOP-REAL 2: |.a.| < rr}; then A17: x in L by XBOOLE_0:def 5; UBD L~f is_outside_component_of L~f by JORDAN2C:68; then P = UBD L~f by A2,JORDAN2C:119; hence thesis by A17,A15,A16,TARSKI:def 4; end; begin :: Go-boards theorem for f being FinSequence of TOP-REAL n st L~f <> {} holds 2 <= len f proof let f be FinSequence of TOP-REAL n; assume L~f <> {}; then len f <> 0 & len f <> 1 by TOPREAL1:22; then len f > 1 by NAT_1:25; then len f >= 1 + 1 by NAT_1:13; hence thesis; end; theorem Th3: 1 <= i & i < len G & 1 <= j & j < width G implies cell(G,i,j) = product ((1,2) --> ([.G*(i,1)`1,G*(i+1,1)`1.],[.G*(1,j)`2,G*(1,j+1)`2.])) proof A1: [.G*(1,j)`2,G*(1,j+1)`2.] = {b where b is Real : G*(1,j)`2 <= b & b <= G *(1,j+1)`2 } by RCOMP_1:def 1; set f = (1,2) --> ([.G*(i,1)`1,G*(i+1,1)`1.],[.G*(1,j)`2,G*(1,j+1)`2.]); A2: dom f = {1,2} by FUNCT_4:62; assume 1 <= i & i < len G & 1 <= j & j < width G; then A3: cell(G,i,j) = { |[r,s]| where r, s is Real: G*(i,1)`1 <= r & r <= G*(i+1 ,1)`1 & G*(1,j)`2 <= s & s <= G*(1,j+1)`2 } by GOBRD11:32; A4: [.G*(i,1)`1,G*(i+1,1)`1.] = {a where a is Real : G*(i,1)`1 <= a & a <= G *(i+1,1)`1 } by RCOMP_1:def 1; thus cell(G,i,j) c= product f proof let c be object; assume c in cell(G,i,j); then consider r, s being Real such that A5: c = |[r,s]| and A6: G*(i,1)`1 <= r & r <= G*(i+1,1)`1 & G*(1,j)`2 <= s & s <= G*(1,j+1 )`2 by A3; A7: r in [.G*(i,1)`1,G*(i+1,1)`1.] & s in [.G*(1,j)`2,G*(1,j+1)`2.] by A4,A1,A6 ; A8: for x being object st x in dom f holds <*r,s*>.x in f.x proof let x be object; A9: s = |[r,s]|`2 by EUCLID:52 .= <*r,s*>.2; assume x in dom f; then A10: x = 1 or x = 2 by TARSKI:def 2; r = |[r,s]|`1 by EUCLID:52 .= <*r,s*>.1; hence thesis by A7,A10,A9,FUNCT_4:63; end; dom <*r,s*> = {1,2} by FINSEQ_1:2,89; hence thesis by A2,A5,A8,CARD_3:9; end; let c be object; assume c in product f; then consider g being Function such that A11: c = g and A12: dom g = dom f and A13: for x being object st x in dom f holds g.x in f.x by CARD_3:def 5; 2 in dom f by A2,TARSKI:def 2; then g.2 in f.2 by A13; then g.2 in [.G*(1,j)`2,G*(1,j+1)`2.] by FUNCT_4:63; then consider b being Real such that A14: g.2 = b and A15: G*(1,j)`2 <= b & b <= G*(1,j+1)`2 by A1; 1 in dom f by A2,TARSKI:def 2; then g.1 in f.1 by A13; then g.1 in [.G*(i,1)`1,G*(i+1,1)`1.] by FUNCT_4:63; then consider a being Real such that A16: g.1 = a and A17: G*(i,1)`1 <= a & a <= G*(i+1,1)`1 by A4; A18: for k being object st k in dom g holds g.k = <*a,b*>.k proof let k be object; assume k in dom g; then k = 1 or k = 2 by A12,TARSKI:def 2; hence thesis by A16,A14,FINSEQ_1:44; end; dom <*a,b*> = {1,2} by FINSEQ_1:2,89; then c = |[a,b]| by A11,A12,A18,FUNCT_1:2,FUNCT_4:62; hence thesis by A3,A17,A15; end; theorem 1 <= i & i < len G & 1 <= j & j < width G implies cell(G,i,j) is compact proof assume 1 <= i & i < len G & 1 <= j & j < width G; then cell(G,i,j) = product ((1,2) --> ([.G*(i,1)`1,G*(i+1,1)`1.], [.G*(1,j)`2 ,G*(1,j+1)`2.])) by Th3; hence thesis by TOPREAL6:78; end; theorem [i,j] in Indices G & [i+n,j] in Indices G implies dist(G*(i,j),G*(i+n, j)) = G*(i+n,j)`1 - G*(i,j)`1 proof assume that A1: [i,j] in Indices G and A2: [i+n,j] in Indices G; set x = G*(i,j), y = G*(i+n,j); per cases; suppose n = 0; hence thesis by TOPREAL6:93; end; suppose A3: n <> 0; A4: i+n <= len G by A2,MATRIX_0:32; A5: 1 <= i by A1,MATRIX_0:32; A6: 1 <= i+n by A2,MATRIX_0:32; A7: 1 <= j & j <= width G by A1,MATRIX_0:32; 1 <= n by A3,NAT_1:14; then i < i+n by NAT_1:19; then x`1 < y`1 by A4,A7,A5,GOBOARD5:3; then A8: x`1 - x`1 < y`1 - x`1 by XREAL_1:14; i <= len G by A1,MATRIX_0:32; then A9: x`2 = G*(1,j)`2 by A7,A5,GOBOARD5:1 .= y`2 by A6,A4,A7,GOBOARD5:1; thus dist(G*(i,j),G*(i+n,j)) = sqrt ((x`1-y`1)^2 + (x`2-y`2)^2) by TOPREAL6:92 .= |.x`1-y`1.| by A9,COMPLEX1:72 .= |.-(x`1-y`1).| by COMPLEX1:52 .= G*(i+n,j)`1 - G*(i,j)`1 by A8,ABSVALUE:def 1; end; end; theorem [i,j] in Indices G & [i,j+n] in Indices G implies dist(G*(i,j),G*(i,j+ n)) = G*(i,j+n)`2 - G*(i,j)`2 proof assume that A1: [i,j] in Indices G and A2: [i,j+n] in Indices G; set x = G*(i,j), y = G*(i,j+n); per cases; suppose n = 0; hence thesis by TOPREAL6:93; end; suppose A3: n <> 0; A4: j+n <= width G by A2,MATRIX_0:32; A5: 1 <= i & i <= len G by A1,MATRIX_0:32; A6: 1 <= j+n by A2,MATRIX_0:32; A7: 1 <= j by A1,MATRIX_0:32; 1 <= n by A3,NAT_1:14; then j < j+n by NAT_1:19; then x`2 < y`2 by A4,A7,A5,GOBOARD5:4; then A8: x`2 - x`2 < y`2 - x`2 by XREAL_1:14; j <= width G by A1,MATRIX_0:32; then A9: x`1 = G*(i,1)`1 by A7,A5,GOBOARD5:2 .= y`1 by A6,A4,A5,GOBOARD5:2; thus dist(G*(i,j),G*(i,j+n)) = sqrt ((x`1-y`1)^2 + (x`2-y`2)^2) by TOPREAL6:92 .= |.x`2-y`2.| by A9,COMPLEX1:72 .= |.-(x`2-y`2).| by COMPLEX1:52 .= G*(i,j+n)`2 - G*(i,j)`2 by A8,ABSVALUE:def 1; end; end; theorem 3 <= len Gauge(C,n)-'1 proof set G = Gauge(C,n); 4 <= len G by JORDAN8:10; then 4 - 1 <= len G-1 by XREAL_1:13; hence thesis by XREAL_0:def 2; end; theorem i <= j implies for a, b being Nat st 2 <= a & a <= len Gauge(C,i) - 1 & 2 <= b & b <= len Gauge(C,i) - 1 ex c, d being Nat st 2 <= c & c <= len Gauge(C,j) - 1 & 2 <= d & d <= len Gauge(C,j) - 1 & [c,d] in Indices Gauge(C,j) & Gauge(C,i)*(a,b) = Gauge(C,j)*(c,d) & c = 2 + 2|^(j-'i) *(a-'2) & d = 2 + 2|^(j-'i)*(b-'2) proof A1: 0 <> 2|^i by NEWTON:83; assume A2: i <= j; then A3: 2|^(j-'i)*(2|^i) = 2|^j / 2|^i*(2|^i) by TOPREAL6:10 .= 2|^j by A1,XCMPLX_1:87; let a, b be Nat such that A4: 2 <= a and A5: a <= len Gauge(C,i) - 1 and A6: 2 <= b and A7: b <= len Gauge(C,i) - 1; A8: 1 <= a & 1 <= b by A4,A6,XXREAL_0:2; set c = 2 + 2|^(j-'i)*(a-'2), d = 2 + 2|^(j-'i)*(b-'2); A9: 0 <= b-2 by A6,XREAL_1:48; set n = N-bound C, e = E-bound C, s = S-bound C, w = W-bound C; A10: 0 <> 2|^j by NEWTON:83; A11: (n-s)/(2|^j)*(d-2) = (n-s)/(2|^j)*((2|^j/2|^i)*(b-'2)) by A2,TOPREAL6:10 .= (n-s)/(2|^j)*(2|^j/2|^i)*(b-'2) .= (n-s)/((2|^j)/(2|^j/2|^i))*(b-'2) by XCMPLX_1:81 .= (n-s)/(2|^i)*(b-'2) by A10,XCMPLX_1:52 .= (n-s)/(2|^i)*(b-2) by A9,XREAL_0:def 2; take c, d; A12: 2+0 <= 2+2|^(j-'i)*(a-'2) by XREAL_1:6; then A13: 1 <= c by XXREAL_0:2; 2|^i + 2 - 2 >= 0; then A14: 2|^i + 2 -' 2 = 2|^i + 0 by XREAL_0:def 2; A15: 0 <= a-2 by A4,XREAL_1:48; A16: (e-w)/(2|^j)*(c-2) = (e-w)/(2|^j)*((2|^j/2|^i)*(a-'2)) by A2,TOPREAL6:10 .= (e-w)/(2|^j)*(2|^j/2|^i)*(a-'2) .= (e-w)/((2|^j)/(2|^j/2|^i))*(a-'2) by XCMPLX_1:81 .= (e-w)/(2|^i)*(a-'2) by A10,XCMPLX_1:52 .= (e-w)/(2|^i)*(a-2) by A15,XREAL_0:def 2; A17: len Gauge(C,j) - 1 < len Gauge(C,j) - 0 by XREAL_1:15; A18: len Gauge(C,i) - 1 = 2|^i + 3 - 1 by JORDAN8:def 1 .= 2|^i + 2; then a -' 2 <= 2|^i + 2 -' 2 by A5,NAT_D:42; then A19: 2|^(j-'i)*(a-'2) <= 2|^j by A14,A3,XREAL_1:64; b -' 2 <= 2|^i + 2 -' 2 by A7,A18,NAT_D:42; then A20: 2|^(j-'i)*(b-'2) <= 2|^j by A14,A3,XREAL_1:64; A21: len Gauge(C,i) - 1 < len Gauge(C,i) - 0 by XREAL_1:15; then A22: a <= len Gauge(C,i) by A5,XXREAL_0:2; len Gauge(C,j) - 1 = 2|^j + 3 - 1 by JORDAN8:def 1 .= 2|^j + 2; hence A23: 2 <= c & c <= len Gauge(C,j) - 1 & 2 <= d & d <= len Gauge(C,j ) - 1 by A19,A20,A12,XREAL_1:6; then A24: 1 <= d by XXREAL_0:2; width Gauge(C,j) = len Gauge(C,j) by JORDAN8:def 1; then A25: d <= width Gauge(C,j) by A23,A17,XXREAL_0:2; c <= len Gauge(C,j) by A23,A17,XXREAL_0:2; hence [c,d] in Indices Gauge(C,j) by A13,A24,A25,MATRIX_0:30; then A26: Gauge(C,j)*(c,d) = |[w+(e-w)/(2|^j)*(c-2), s+(n-s)/(2|^j)*(d-2)]| by JORDAN8:def 1; width Gauge(C,i) = len Gauge(C,i) by JORDAN8:def 1; then b <= width Gauge(C,i) by A7,A21,XXREAL_0:2; then [a,b] in Indices Gauge(C,i) by A22,A8,MATRIX_0:30; then A27: Gauge(C,i)*(a,b) = |[w+(e-w)/(2|^i)*(a-2), s+(n-s)/(2|^i)*(b-2)]| by JORDAN8:def 1; then A28: Gauge(C,i)*(a,b)`2 = s+(n-s)/(2|^i)*(b-2) by EUCLID:52 .= Gauge(C,j)*(c,d)`2 by A26,A11,EUCLID:52; Gauge(C,i)*(a,b)`1 = w+(e-w)/(2|^i)*(a-2) by A27,EUCLID:52 .= Gauge(C,j)*(c,d)`1 by A26,A16,EUCLID:52; hence Gauge(C,i)*(a,b) = Gauge(C,j)*(c,d) by A28,TOPREAL3:6; thus thesis; end; theorem Th9: [i,j] in Indices Gauge(C,n) & [i,j+1] in Indices Gauge(C,n) implies dist(Gauge(C,n)*(i,j),Gauge(C,n)*(i,j+1)) = (N-bound C - S-bound C)/2|^ n proof set G = Gauge(C,n), a = N-bound C, e = E-bound C, s = S-bound C, w = W-bound C, p1 = G*(i,j), p2 = G*(i,j+1); assume that A1: [i,j] in Indices G and A2: [i,j+1] in Indices G; A3: p2 = |[w+(e-w)/(2|^n)*(i-2), s+(a-s)/(2|^n)*(j+1-2)]| by A2,JORDAN8:def 1; a >= s by SPRECT_1:22; then A4: a - s >= s - s by XREAL_1:9; set x = (a-s)/(2|^n); consider p, q being Point of Euclid 2 such that A5: p = p1 & q = p2 and A6: dist(p1,p2) = dist(p,q) by TOPREAL6:def 1; A7: p1 = |[w+(e-w)/(2|^n)*(i-2), s+(a-s)/(2|^n)*(j-2)]| by A1,JORDAN8:def 1; dist(p,q) = (Pitag_dist 2).(p,q) by METRIC_1:def 1 .= sqrt ((p1`1 - p2`1)^2 + (p1`2 - p2`2)^2) by A5,TOPREAL3:7 .= sqrt ((w+(e-w)/(2|^n)*(i-2) - p2`1)^2 + (p1`2 - p2`2)^2) by A7,EUCLID:52 .= sqrt ((w+(e-w)/(2|^n)*(i-2) - (w+(e-w)/(2|^n)*(i-2)))^2 + (p1`2 - p2 `2)^2) by A3,EUCLID:52 .= |.p1`2 - p2`2.| by COMPLEX1:72 .= |.s+x*(j-2) - p2`2.| by A7,EUCLID:52 .= |.s+x*(j-2) - (s+x*(j+1-2)).| by A3,EUCLID:52 .= |.-x.| .= |.x.| by COMPLEX1:52 .= |.a-s.|/|.2|^n.| by COMPLEX1:67 .= (a-s)/|.2|^n.| by A4,ABSVALUE:def 1; hence thesis by A6,ABSVALUE:def 1; end; theorem Th10: [i,j] in Indices Gauge(C,n) & [i+1,j] in Indices Gauge(C,n) implies dist(Gauge(C,n)*(i,j),Gauge(C,n)*(i+1,j)) = (E-bound C - W-bound C)/2|^ n proof set G = Gauge(C,n), a = N-bound C, e = E-bound C, s = S-bound C, w = W-bound C, p1 = G*(i,j), p2 = G*(i+1,j); assume that A1: [i,j] in Indices G and A2: [i+1,j] in Indices G; A3: p2 = |[w+(e-w)/(2|^n)*(i+1-2), s+(a-s)/(2|^n)*(j-2)]| by A2,JORDAN8:def 1; e >= w by SPRECT_1:21; then A4: e - w >= w - w by XREAL_1:9; set x = (e-w)/(2|^n); consider p, q being Point of Euclid 2 such that A5: p = p1 & q = p2 and A6: dist(p1,p2) = dist(p,q) by TOPREAL6:def 1; A7: p1 = |[w+(e-w)/(2|^n)*(i-2), s+(a-s)/(2|^n)*(j-2)]| by A1,JORDAN8:def 1; dist(p,q) = (Pitag_dist 2).(p,q) by METRIC_1:def 1 .= sqrt ((p1`1 - p2`1)^2 + (p1`2 - p2`2)^2) by A5,TOPREAL3:7 .= sqrt ((p1`1 - p2`1)^2 + (s+(a-s)/(2|^n)*(j-2) - p2`2)^2) by A7,EUCLID:52 .= sqrt ((p1`1 - p2`1)^2 + (s+(a-s)/(2|^n)*(j-2) - (s+(a-s)/(2|^n)*(j-2) ))^2) by A3,EUCLID:52 .= |.p1`1 - p2`1.| by COMPLEX1:72 .= |.w+x*(i-2) - p2`1.| by A7,EUCLID:52 .= |.w+x*(i-2) - (w+x*(i+1-2)).| by A3,EUCLID:52 .= |.-x.| .= |.x.| by COMPLEX1:52 .= |.e-w.|/|.2|^n.| by COMPLEX1:67 .= (e-w)/|.2|^n.| by A4,ABSVALUE:def 1; hence thesis by A6,ABSVALUE:def 1; end; theorem for r, t being Real holds r > 0 & t > 0 implies ex n being Nat st 1 < 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 r, t be Real; assume that A1: r > 0 and A2: t > 0; set n = N-bound C, e = E-bound C, s = S-bound C, w = W-bound C; set a = |.[\ log(2,(n-s)/r) /].| + 1, b = |.[\ log(2,(e-w)/t) /].| + 1; take i = max(a,b)+1; A3: 2 to_power i > 0 by POWER:34; then A4: 2|^i > 0 by POWER:41; [\ log(2,(n-s)/r) /] <= |.[\ log(2,(n-s)/r) /].| by ABSVALUE:4; then A5: [\ log(2,(n-s)/r) /] + 1 <= a by XREAL_1:6; [\ log(2,(n-s)/r) /] > log(2,(n-s)/r) - 1 by INT_1:def 6; then [\ log(2,(n-s)/r) /] + 1 > log(2,(n-s)/r) - 1 + 1 by XREAL_1:6; then A6: a > log(2,(n-s)/r) - 1 + 1 by A5,XXREAL_0:2; a <= max(a,b) by XXREAL_0:25; then A7: a+1 <= max(a,b)+1 by XREAL_1:6; a < a+1 by XREAL_1:29; then i > a by A7,XXREAL_0:2; then i > log(2,(n-s)/r) by A6,XXREAL_0:2; then log(2,2 to_power i) > log(2,(n-s)/r) by A3,POWER:def 3; then 2 to_power i > (n-s)/r by A3,PRE_FF:10; then 2|^i > (n-s)/r by POWER:41; then 2|^i * r > (n-s)/r * r by A1,XREAL_1:68; then 2|^i * r > n-s by A1,XCMPLX_1:87; then 2|^i * r / 2|^i > (n-s) / 2|^i by A4,XREAL_1:74; then A8: (n-s)/2|^i < r by A4,XCMPLX_1:89; a >= 0+1 & max(a,b) >= a by XREAL_1:7,XXREAL_0:25; then max(a,b) >= 1 by XXREAL_0:2; then max(a,b)+1 >= 1+1 by XREAL_1:7; hence 1 < i by XXREAL_0:2; A9: len Gauge(C,i) >= 4 by JORDAN8:10; then A10: 1 <= len Gauge(C,i) by XXREAL_0:2; [\ log(2,(e-w)/t) /] <= |.[\ log(2,(e-w)/t) /].| by ABSVALUE:4; then A11: [\ log(2,(e-w)/t) /] + 1 <= b by XREAL_1:6; [\ log(2,(e-w)/t) /] > log(2,(e-w)/t) - 1 by INT_1:def 6; then [\ log(2,(e-w)/t) /] + 1 > log(2,(e-w)/t) - 1 + 1 by XREAL_1:6; then A12: b > log(2,(e-w)/t) - 1 + 1 by A11,XXREAL_0:2; b <= max(a,b) by XXREAL_0:25; then A13: b+1 <= max(a,b)+1 by XREAL_1:6; b < b+1 by XREAL_1:29; then i > b by A13,XXREAL_0:2; then i > log(2,(e-w)/t) by A12,XXREAL_0:2; then log(2,2 to_power i) > log(2,(e-w)/t) by A3,POWER:def 3; then 2 to_power i > (e-w)/t by A3,PRE_FF:10; then 2|^i > (e-w)/t by POWER:41; then 2|^i * t > (e-w)/t * t by A2,XREAL_1:68; then 2|^i * t > e-w by A2,XCMPLX_1:87; then 2|^i * t / 2|^i > (e-w) / 2|^i by A4,XREAL_1:74; then A14: (e-w)/2|^i < t by A4,XCMPLX_1:89; A15: len Gauge(C,i) = width Gauge(C,i) by JORDAN8:def 1; then A16: [1,1] in Indices Gauge(C,i) by A10,MATRIX_0:30; A17: 1+1 <= width Gauge(C,i) by A15,A9,XXREAL_0:2; then A18: [1,1+1] in Indices Gauge(C,i) by A10,MATRIX_0:30; [1+1,1] in Indices Gauge(C,i) by A15,A10,A17,MATRIX_0:30; hence thesis by A8,A14,A16,A18,Th9,Th10; end; begin :: LeftComp and RightComp theorem Th12: for P being Subset of (TOP-REAL 2)|(L~f)` st P is a_component holds P = RightComp f or P = LeftComp f proof let P be Subset of (TOP-REAL 2)|(L~f)`; assume that A1: P is a_component and A2: P <> RightComp f; P <> {}((TOP-REAL 2)|(L~f)`) by A1,CONNSP_1:32; then consider a being Point of (TOP-REAL 2)|(L~f)` such that A3: a in P by SUBSET_1:4; the carrier of (TOP-REAL 2)|(L~f)` = (L~f)` & (L~f)` = LeftComp f \/ RightComp f by GOBRD12:10,PRE_TOPC:8; then A4: a in LeftComp f or a in RightComp f by XBOOLE_0:def 3; LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1; then A5: ex L being Subset of (TOP-REAL 2)|(L~f)` st L = LeftComp f & L is a_component by CONNSP_1:def 6; RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2; then consider R being Subset of (TOP-REAL 2)|(L~f)` such that A6: R = RightComp f and A7: R is a_component by CONNSP_1:def 6; P misses R by A1,A2,A6,A7,CONNSP_1:35; then P meets LeftComp f by A6,A3,A4,XBOOLE_0:3; hence thesis by A1,A5,CONNSP_1:35; end; theorem for A1, A2 being Subset of TOP-REAL 2 st (L~f)` = A1 \/ A2 & A1 misses A2 & for C1, C2 being Subset of (TOP-REAL 2)|(L~f)` st C1 = A1 & C2 = A2 holds C1 is a_component & C2 is a_component holds A1 = RightComp f & A2 = LeftComp f or A1 = LeftComp f & A2 = RightComp f proof let A1, A2 be Subset of TOP-REAL 2 such that A1: (L~f)` = A1 \/ A2 and A2: A1 /\ A2 = {} and A3: for C1, C2 being Subset of (TOP-REAL 2)|(L~f)` st C1 = A1 & C2 = A2 holds C1 is a_component & C2 is a_component; the carrier of (TOP-REAL 2)|(L~f)` = (L~f)` by PRE_TOPC:8; then reconsider C1 = A1, C2 = A2 as Subset of (TOP-REAL 2)|(L~f)` by A1, XBOOLE_1:7; C1 = A1; then C2 is a_component by A3; then A4: C2 = RightComp f or C2 = LeftComp f by Th12; C2 = A2; then C1 is a_component by A3; then A5: C1 = RightComp f or C1 = LeftComp f by Th12; assume not thesis; hence contradiction by A2,A5,A4; end; theorem Th14: LeftComp f misses RightComp f proof assume LeftComp f /\ RightComp f <> {}; then consider x being object such that A1: x in LeftComp f /\ RightComp f by XBOOLE_0:def 1; now take x; thus x in LeftComp f & x in RightComp f by A1,XBOOLE_0:def 4; end; then A2: LeftComp f meets RightComp f by XBOOLE_0:3; LeftComp f is_a_component_of (L~f)` & RightComp f is_a_component_of (L~f ) ` by GOBOARD9:def 1,def 2; hence thesis by A2,GOBOARD9:1,SPRECT_4:6; end; theorem Th15: L~f \/ RightComp f \/ LeftComp f = the carrier of TOP-REAL 2 proof A1: (L~f)` \/ L~f = [#]the carrier of TOP-REAL 2 by SUBSET_1:10 .= the carrier of TOP-REAL 2; (L~f)` = RightComp f \/ LeftComp f by GOBRD12:10; hence thesis by A1,XBOOLE_1:4; end; theorem Th16: p in L~f iff not p in LeftComp f & not p in RightComp f proof A1: p in L~f iff not p in (L~f)` by XBOOLE_0:def 5; (L~f)` = LeftComp f \/ RightComp f by GOBRD12:10; hence thesis by A1,XBOOLE_0:def 3; end; theorem Th17: p in LeftComp f iff not p in L~f & not p in RightComp f proof LeftComp f misses RightComp f by Th14; then A1: (L~f)` = LeftComp f \/ RightComp f & LeftComp f /\ RightComp f = {} by GOBRD12:10; p in L~f iff not p in (L~f)` by XBOOLE_0:def 5; hence thesis by A1,XBOOLE_0:def 3,def 4; end; theorem p in RightComp f iff not p in L~f & not p in LeftComp f by Th16,Th17; theorem Th19: L~f = (Cl RightComp f) \ RightComp f proof thus L~f c= (Cl RightComp f) \ RightComp f proof let x be object; assume A1: x in L~f; then reconsider p = x as Point of TOP-REAL 2; consider i such that A2: 1 <= i & i+1 <= len f and A3: p in LSeg(f,i) by A1,SPPOL_2:13; for O being Subset of TOP-REAL 2 st O is open holds p in O implies RightComp f meets O proof left_cell(f,i) /\ right_cell(f,i) = LSeg(f,i) by A2,GOBOARD5:31; then LSeg(f,i) c= right_cell(f,i) by XBOOLE_1:17; then A4: p in right_cell(f,i) by A3; f is_sequence_on GoB f by GOBOARD5:def 5; then consider i1, j1, i2, j2 being Nat such that A5: [i1,j1] in Indices GoB f and A6: f/.i = GoB f*(i1,j1) and A7: [i2,j2] in Indices GoB f and A8: f/.(i+1) = GoB f*(i2,j2) and A9: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A2,JORDAN8:3; A10: 1 <= i1 by A5,MATRIX_0:32; A11: j2 <= width GoB f by A7,MATRIX_0:32; A12: 1 <= j1 by A5,MATRIX_0:32; A13: j1 <= width GoB f by A5,MATRIX_0:32; A14: i1 <= len GoB f by A5,MATRIX_0:32; A15: i2 <= len GoB f by A7,MATRIX_0:32; A16: now per cases by A9; case A17: i1 = i2 & j1+1 = j2; set w = i1-'1; A18: w+1 = i1 by A10,XREAL_1:235; then right_cell(f,i) = cell(GoB f,w+1,j1) by A2,A5,A6,A7,A8,A17, GOBOARD5:27; hence p in Cl Int right_cell(f,i) by A4,A14,A13,A18,GOBRD11:35; end; case A19: i1+1 = i2 & j1 = j2; set w = j1-'1; w <= w+1 & w+1 <= width GoB f by A12,A13,NAT_1:11,XREAL_1:235; then A20: w <= width GoB f by XXREAL_0:2; w+1 = j1 by A12,XREAL_1:235; then right_cell(f,i) = cell(GoB f,i1,w) by A2,A5,A6,A7,A8,A19, GOBOARD5:28; hence p in Cl Int right_cell(f,i) by A4,A14,A20,GOBRD11:35; end; case A21: i1 = i2+1 & j1 = j2; set w = j1-'1; A22: w+1 = j1 by A12,XREAL_1:235; then right_cell(f,i) = cell(GoB f,i2,w+1) by A2,A5,A6,A7,A8,A21, GOBOARD5:29; hence p in Cl Int right_cell(f,i) by A4,A13,A15,A22,GOBRD11:35; end; case A23: i1 = i2 & j1 = j2+1; set z = i1-'1; z <= z+1 & z+1 <= len GoB f by A10,A14,NAT_1:11,XREAL_1:235; then A24: z <= len GoB f by XXREAL_0:2; z+1 = i1 by A10,XREAL_1:235; then right_cell(f,i) = cell(GoB f,z,j2) by A2,A5,A6,A7,A8,A23, GOBOARD5:30; hence p in Cl Int right_cell(f,i) by A4,A11,A24,GOBRD11:35; end; end; let O be Subset of TOP-REAL 2; assume O is open & p in O; then O meets Int right_cell(f,i) by A16,PRE_TOPC:def 7; hence thesis by A2,GOBOARD9:25,XBOOLE_1:63; end; then A25: p in Cl RightComp f by PRE_TOPC:def 7; not x in RightComp f by A1,Th16; hence thesis by A25,XBOOLE_0:def 5; end; assume not (Cl RightComp f) \ RightComp f c= L~f; then consider q being object such that A26: q in (Cl RightComp f) \ RightComp f and A27: not q in L~f; reconsider q as Point of TOP-REAL 2 by A26; not q in RightComp f by A26,XBOOLE_0:def 5; then A28: q in LeftComp f by A27,Th16; q in Cl RightComp f by A26,XBOOLE_0:def 5; then LeftComp f meets RightComp f by A28,PRE_TOPC:def 7; hence contradiction by Th14; end; theorem Th20: L~f = (Cl LeftComp f) \ LeftComp f proof thus L~f c= (Cl LeftComp f) \ LeftComp f proof let x be object; assume A1: x in L~f; then reconsider p = x as Point of TOP-REAL 2; consider i such that A2: 1 <= i & i+1 <= len f and A3: p in LSeg(f,i) by A1,SPPOL_2:13; for O being Subset of TOP-REAL 2 st O is open holds p in O implies LeftComp f meets O proof left_cell(f,i) /\ right_cell(f,i) = LSeg(f,i) by A2,GOBOARD5:31; then LSeg(f,i) c= left_cell(f,i) by XBOOLE_1:17; then A4: p in left_cell(f,i) by A3; f is_sequence_on GoB f by GOBOARD5:def 5; then consider i1, j1, i2, j2 being Nat such that A5: [i1,j1] in Indices GoB f and A6: f/.i = GoB f*(i1,j1) and A7: [i2,j2] in Indices GoB f and A8: f/.(i+1) = GoB f*(i2,j2) and A9: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A2,JORDAN8:3; A10: 1 <= i1 by A5,MATRIX_0:32; A11: j2 <= width GoB f by A7,MATRIX_0:32; A12: 1 <= j1 by A5,MATRIX_0:32; A13: j1 <= width GoB f by A5,MATRIX_0:32; A14: i1 <= len GoB f by A5,MATRIX_0:32; A15: i2 <= len GoB f by A7,MATRIX_0:32; A16: now per cases by A9; case A17: i1 = i2 & j1+1 = j2; set w = i1-'1; w <= w+1 & w+1 <= len GoB f by A10,A14,NAT_1:11,XREAL_1:235; then A18: w <= len GoB f by XXREAL_0:2; w+1 = i1 by A10,XREAL_1:235; then left_cell(f,i) = cell(GoB f,w,j1) by A2,A5,A6,A7,A8,A17, GOBOARD5:27; hence p in Cl Int left_cell(f,i) by A4,A13,A18,GOBRD11:35; end; case A19: i1+1 = i2 & j1 = j2; set w = j1-'1; w+1 = j1 by A12,XREAL_1:235; then A20: left_cell(f,i) = cell(GoB f,i1,w+1) by A2,A5,A6,A7,A8,A19,GOBOARD5:28 ; w+1 <= width GoB f by A12,A13,XREAL_1:235; hence p in Cl Int left_cell(f,i) by A4,A14,A20,GOBRD11:35; end; case A21: i1 = i2+1 & j1 = j2; set w = j1-'1; w <= w+1 & w+1 <= width GoB f by A12,A13,NAT_1:11,XREAL_1:235; then A22: w <= width GoB f by XXREAL_0:2; w+1 = j1 by A12,XREAL_1:235; then left_cell(f,i) = cell(GoB f,i2,w) by A2,A5,A6,A7,A8,A21, GOBOARD5:29; hence p in Cl Int left_cell(f,i) by A4,A15,A22,GOBRD11:35; end; case A23: i1 = i2 & j1 = j2+1; set z = i1-'1; z+1 = i1 by A10,XREAL_1:235; then A24: left_cell(f,i) = cell(GoB f,z+1,j2) by A2,A5,A6,A7,A8,A23,GOBOARD5:30 ; z+1 <= len GoB f by A10,A14,XREAL_1:235; hence p in Cl Int left_cell(f,i) by A4,A11,A24,GOBRD11:35; end; end; let O be Subset of TOP-REAL 2; assume O is open & p in O; then O meets Int left_cell(f,i) by A16,PRE_TOPC:def 7; hence thesis by A2,GOBOARD9:21,XBOOLE_1:63; end; then A25: p in Cl LeftComp f by PRE_TOPC:def 7; not x in LeftComp f by A1,Th16; hence thesis by A25,XBOOLE_0:def 5; end; assume not (Cl LeftComp f) \ LeftComp f c= L~f; then consider q being object such that A26: q in (Cl LeftComp f) \ LeftComp f and A27: not q in L~f; reconsider q as Point of TOP-REAL 2 by A26; not q in LeftComp f by A26,XBOOLE_0:def 5; then A28: q in RightComp f by A27,Th16; q in Cl LeftComp f by A26,XBOOLE_0:def 5; then RightComp f meets LeftComp f by A28,PRE_TOPC:def 7; hence contradiction by Th14; end; theorem Th21: Cl RightComp f = (RightComp f) \/ L~f proof thus Cl RightComp f c= RightComp f \/ L~f proof let x be object; assume A1: x in Cl RightComp f; now A2: now assume x in LeftComp f; then LeftComp f meets RightComp f by A1,TOPS_1:12; hence contradiction by Th14; end; assume not x in RightComp f; hence x in L~f by A1,A2,Th16; end; hence thesis by XBOOLE_0:def 3; end; (Cl RightComp f) \ RightComp f c= Cl RightComp f by XBOOLE_1:36; then RightComp f c= Cl RightComp f & L~f c= Cl RightComp f by Th19, PRE_TOPC:18; hence thesis by XBOOLE_1:8; end; theorem Cl LeftComp f = (LeftComp f) \/ L~f proof thus Cl LeftComp f c= LeftComp f \/ L~f proof let x be object; assume A1: x in Cl LeftComp f; now A2: not x in RightComp f by A1,Th14,TOPS_1:12; assume not x in LeftComp f; hence x in L~f by A1,A2,Th16; end; hence thesis by XBOOLE_0:def 3; end; (Cl LeftComp f) \ LeftComp f c= Cl LeftComp f by XBOOLE_1:36; then LeftComp f c= Cl LeftComp f & L~f c= Cl LeftComp f by Th20,PRE_TOPC:18; hence thesis by XBOOLE_1:8; end; registration let f be non constant standard special_circular_sequence; cluster L~f -> Jordan; coherence proof thus (L~f)` <> {}; take A1 = RightComp f, A2 = LeftComp f; thus (L~f)` = A1 \/ A2 by GOBRD12:10; L~f = (Cl A1) \ A1 by Th19; hence thesis by Th14,Th20,GOBOARD9:def 1,def 2; end; end; reserve f for clockwise_oriented non constant standard special_circular_sequence; theorem Th23: p in RightComp f implies W-bound L~f < p`1 proof set g = Rotate(f,N-min L~f); A1: L~f = L~g by REVROT_1:33; reconsider u = p as Point of Euclid 2 by EUCLID:22; assume p in RightComp f; then p in RightComp g by REVROT_1:37; then u in Int RightComp g by TOPS_1:23; then consider r being Real such that A2: r > 0 and A3: Ball(u,r) c= RightComp g by GOBOARD6:5; reconsider r as Real; reconsider k = |[p`1-r/2,p`2]| as Point of Euclid 2 by EUCLID:22; dist(u,k) = (Pitag_dist 2).(u,k) by METRIC_1:def 1 .= sqrt ((p`1 - |[p`1-r/2,p`2]|`1)^2 + (p`2 - |[p`1-r/2,p`2]|`2)^2) by TOPREAL3:7 .= sqrt ((p`1 - (p`1-r/2))^2 + (p`2 - |[p`1-r/2,p`2]|`2)^2) by EUCLID:52 .= sqrt ((p`1 - (p`1-r/2))^2 + (p`2 - p`2)^2) by EUCLID:52 .= r/2 by A2,SQUARE_1:22; then dist(u,k) < r/1 by A2,XREAL_1:76; then A4: k in Ball(u,r) by METRIC_1:11; RightComp g misses LeftComp g by Th14; then A5: not |[p`1-r/2,p`2]| in LeftComp g by A3,A4,XBOOLE_0:3; set x = |[p`1-r/2,N-bound L~SpStSeq L~g]|; A6: LSeg(NW-corner L~g,NE-corner L~g) c= L~SpStSeq L~g by SPRECT_3:14; A7: proj1.x = x`1 by PSCOMP_1:def 5 .= p`1-r/2 by EUCLID:52; N-min L~f in rng f by SPRECT_2:39; then A8: g/.1 = N-min L~g by A1,FINSEQ_6:92; then |[p`1-r/2,p`2]|`1 <= E-bound L~g by A5,JORDAN2C:111; then p`1-r/2 <= E-bound L~g by EUCLID:52; then A9: x`1 <= E-bound L~g by EUCLID:52; x`2 = N-bound L~SpStSeq L~g by EUCLID:52; then A10: x`2 = N-bound L~g by SPRECT_1:60; |[p`1-r/2,p`2]|`1 >= W-bound L~g by A8,A5,JORDAN2C:110; then p`1-r/2 >= W-bound L~g by EUCLID:52; then A11: x`1 >= W-bound L~g by EUCLID:52; LSeg(NW-corner L~g, NE-corner L~g) = { q : q`1 <= E-bound L~g & q`1 >= W-bound L~g & q`2 = N-bound L~g} by SPRECT_1:25; then x in LSeg(NW-corner L~g,NE-corner L~g) by A9,A11,A10; then proj1.:L~SpStSeq L~g is bounded_below & p`1-r/2 in proj1.:L~SpStSeq L~g by A6,A7,FUNCT_2:35; then A12: lower_bound(proj1.:L~SpStSeq L~g) <= p`1-r/2 by SEQ_4:def 2; r/2 > 0 by A2,XREAL_1:139; then A13: p`1-r/2 < p`1-0 by XREAL_1:15; W-bound L~SpStSeq L~g = W-bound L~g & W-bound L~SpStSeq L~g = lower_bound( proj1.:L~SpStSeq L~g) by SPRECT_1:43,58; hence thesis by A1,A12,A13,XXREAL_0:2; end; theorem Th24: p in RightComp f implies E-bound L~f > p`1 proof set g = Rotate(f,N-min L~f); A1: L~f = L~g by REVROT_1:33; reconsider u = p as Point of Euclid 2 by EUCLID:22; assume p in RightComp f; then p in RightComp g by REVROT_1:37; then u in Int RightComp g by TOPS_1:23; then consider r being Real such that A2: r > 0 and A3: Ball(u,r) c= RightComp g by GOBOARD6:5; reconsider r as Real; reconsider k = |[p`1+r/2,p`2]| as Point of Euclid 2 by EUCLID:22; dist(u,k) = (Pitag_dist 2).(u,k) by METRIC_1:def 1 .= sqrt ((p`1 - |[p`1+r/2,p`2]|`1)^2 + (p`2 - |[p`1+r/2,p`2]|`2)^2) by TOPREAL3:7 .= sqrt ((p`1 - (p`1+r/2))^2 + (p`2 - |[p`1+r/2,p`2]|`2)^2) by EUCLID:52 .= sqrt ((p`1 - (p`1+r/2))^2 + (p`2 - p`2)^2) by EUCLID:52 .= sqrt ((r/2)^2) .= r/2 by A2,SQUARE_1:22; then dist(u,k) < r/1 by A2,XREAL_1:76; then A4: k in Ball(u,r) by METRIC_1:11; RightComp g misses LeftComp g by Th14; then A5: not |[p`1+r/2,p`2]| in LeftComp g by A3,A4,XBOOLE_0:3; set x = |[p`1+r/2,N-bound L~SpStSeq L~g]|; A6: LSeg(NW-corner L~g,NE-corner L~g) c= L~SpStSeq L~g by SPRECT_3:14; A7: proj1.x = x`1 by PSCOMP_1:def 5 .= p`1+r/2 by EUCLID:52; N-min L~f in rng f by SPRECT_2:39; then A8: g/.1 = N-min L~g by A1,FINSEQ_6:92; then |[p`1+r/2,p`2]|`1 <= E-bound L~g by A5,JORDAN2C:111; then p`1+r/2 <= E-bound L~g by EUCLID:52; then A9: x`1 <= E-bound L~g by EUCLID:52; x`2 = N-bound L~SpStSeq L~g by EUCLID:52; then A10: x`2 = N-bound L~g by SPRECT_1:60; |[p`1+r/2,p`2]|`1 >= W-bound L~g by A8,A5,JORDAN2C:110; then p`1+r/2 >= W-bound L~g by EUCLID:52; then A11: x`1 >= W-bound L~g by EUCLID:52; LSeg(NW-corner L~g, NE-corner L~g) = { q : q`1 <= E-bound L~g & q`1 >= W-bound L~g & q`2 = N-bound L~g} by SPRECT_1:25; then x in LSeg(NW-corner L~g,NE-corner L~g) by A9,A11,A10; then proj1.:L~SpStSeq L~g is bounded_above & p`1+r/2 in proj1.:L~SpStSeq L~g by A6,A7,FUNCT_2:35; then A12: upper_bound(proj1.:L~SpStSeq L~g) >= p`1+r/2 by SEQ_4:def 1; r/2 > 0 by A2,XREAL_1:139; then A13: p`1+r/2 > p`1+0 by XREAL_1:6; E-bound L~SpStSeq L~g = E-bound L~g & E-bound L~SpStSeq L~g = upper_bound(proj1 .:L~ SpStSeq L~g) by SPRECT_1:46,61; hence thesis by A1,A12,A13,XXREAL_0:2; end; theorem Th25: p in RightComp f implies N-bound L~f > p`2 proof set g = Rotate(f,N-min L~f); A1: L~f = L~g by REVROT_1:33; reconsider u = p as Point of Euclid 2 by EUCLID:22; assume p in RightComp f; then p in RightComp g by REVROT_1:37; then u in Int RightComp g by TOPS_1:23; then consider r being Real such that A2: r > 0 and A3: Ball(u,r) c= RightComp g by GOBOARD6:5; reconsider r as Real; reconsider k = |[p`1,p`2+r/2]| as Point of Euclid 2 by EUCLID:22; dist(u,k) = (Pitag_dist 2).(u,k) by METRIC_1:def 1 .= sqrt ((p`1 - |[p`1,p`2+r/2]|`1)^2 + (p`2 - |[p`1,p`2+r/2]|`2)^2) by TOPREAL3:7 .= sqrt ((p`1 - p`1)^2 + (p`2 - |[p`1,p`2+r/2]|`2)^2) by EUCLID:52 .= sqrt ((p`2 - (p`2+r/2))^2) by EUCLID:52 .= sqrt ((r/2)^2) .= r/2 by A2,SQUARE_1:22; then dist(u,k) < r/1 by A2,XREAL_1:76; then A4: k in Ball(u,r) by METRIC_1:11; RightComp g misses LeftComp g by Th14; then A5: not |[p`1,p`2+r/2]| in LeftComp g by A3,A4,XBOOLE_0:3; set x = |[E-bound L~SpStSeq L~g,p`2+r/2]|; A6: LSeg(SE-corner L~g,NE-corner L~g) c= L~SpStSeq L~g by TOPREAL6:35; A7: proj2.x = x`2 by PSCOMP_1:def 6 .= p`2+r/2 by EUCLID:52; N-min L~f in rng f by SPRECT_2:39; then A8: g/.1 = N-min L~g by A1,FINSEQ_6:92; then |[p`1,p`2+r/2]|`2 <= N-bound L~g by A5,JORDAN2C:113; then p`2+r/2 <= N-bound L~g by EUCLID:52; then A9: x`2 <= N-bound L~g by EUCLID:52; x`1 = E-bound L~SpStSeq L~g by EUCLID:52; then A10: x`1 = E-bound L~g by SPRECT_1:61; |[p`1,p`2+r/2]|`2 >= S-bound L~g by A8,A5,JORDAN2C:112; then p`2+r/2 >= S-bound L~g by EUCLID:52; then A11: x`2 >= S-bound L~g by EUCLID:52; LSeg(SE-corner L~g, NE-corner L~g) = { q : q`1 = E-bound L~g & q`2 <= N-bound L~g & q`2 >= S-bound L~g } by SPRECT_1:23; then x in LSeg(SE-corner L~g,NE-corner L~g) by A9,A11,A10; then proj2.:L~SpStSeq L~g is bounded_above & p`2+r/2 in proj2.:L~SpStSeq L~g by A6,A7,FUNCT_2:35; then A12: upper_bound(proj2.:L~SpStSeq L~g) >= p`2+r/2 by SEQ_4:def 1; r/2 > 0 by A2,XREAL_1:139; then A13: p`2+r/2 > p`2+0 by XREAL_1:6; N-bound L~SpStSeq L~g = N-bound L~g & N-bound L~SpStSeq L~g = upper_bound(proj2 .:L~ SpStSeq L~g) by SPRECT_1:45,60; hence thesis by A1,A12,A13,XXREAL_0:2; end; theorem Th26: p in RightComp f implies S-bound L~f < p`2 proof set g = Rotate(f,N-min L~f); A1: L~f = L~g by REVROT_1:33; reconsider u = p as Point of Euclid 2 by EUCLID:22; assume p in RightComp f; then p in RightComp g by REVROT_1:37; then u in Int RightComp g by TOPS_1:23; then consider r being Real such that A2: r > 0 and A3: Ball(u,r) c= RightComp g by GOBOARD6:5; reconsider r as Real; reconsider k = |[p`1,p`2-r/2]| as Point of Euclid 2 by EUCLID:22; dist(u,k) = (Pitag_dist 2).(u,k) by METRIC_1:def 1 .= sqrt ((p`1 - |[p`1,p`2-r/2]|`1)^2 + (p`2 - |[p`1,p`2-r/2]|`2)^2) by TOPREAL3:7 .= sqrt ((p`1 - p`1)^2 + (p`2 - |[p`1,p`2-r/2]|`2)^2) by EUCLID:52 .= sqrt ((p`2 - (p`2-r/2))^2) by EUCLID:52 .= r/2 by A2,SQUARE_1:22; then dist(u,k) < r/1 by A2,XREAL_1:76; then A4: k in Ball(u,r) by METRIC_1:11; RightComp g misses LeftComp g by Th14; then A5: not |[p`1,p`2-r/2]| in LeftComp g by A3,A4,XBOOLE_0:3; set x = |[E-bound L~SpStSeq L~g,p`2-r/2]|; A6: LSeg(SE-corner L~g,NE-corner L~g) c= L~SpStSeq L~g by TOPREAL6:35; A7: proj2.x = x`2 by PSCOMP_1:def 6 .= p`2-r/2 by EUCLID:52; N-min L~f in rng f by SPRECT_2:39; then A8: g/.1 = N-min L~g by A1,FINSEQ_6:92; then |[p`1,p`2-r/2]|`2 <= N-bound L~g by A5,JORDAN2C:113; then p`2-r/2 <= N-bound L~g by EUCLID:52; then A9: x`2 <= N-bound L~g by EUCLID:52; x`1 = E-bound L~SpStSeq L~g by EUCLID:52; then A10: x`1 = E-bound L~g by SPRECT_1:61; |[p`1,p`2-r/2]|`2 >= S-bound L~g by A8,A5,JORDAN2C:112; then p`2-r/2 >= S-bound L~g by EUCLID:52; then A11: x`2 >= S-bound L~g by EUCLID:52; LSeg(SE-corner L~g, NE-corner L~g) = { q : q`1 = E-bound L~g & q`2 <= N-bound L~g & q`2 >= S-bound L~g } by SPRECT_1:23; then x in LSeg(SE-corner L~g,NE-corner L~g) by A9,A11,A10; then proj2.:L~SpStSeq L~g is bounded_below & p`2-r/2 in proj2.:L~SpStSeq L~g by A6,A7,FUNCT_2:35; then A12: lower_bound(proj2.:L~SpStSeq L~g) <= p`2-r/2 by SEQ_4:def 2; r/2 > 0 by A2,XREAL_1:139; then A13: p`2-r/2 < p`2-0 by XREAL_1:15; S-bound L~SpStSeq L~g = S-bound L~g & S-bound L~SpStSeq L~g = lower_bound( proj2.:L~SpStSeq L~g) by SPRECT_1:44,59; hence thesis by A1,A12,A13,XXREAL_0:2; end; theorem Th27: p in RightComp f & q in LeftComp f implies LSeg(p,q) meets L~f proof assume that A1: p in RightComp f and A2: q in LeftComp f; assume LSeg(p,q) misses L~f; then LSeg(p,q) c= (L~f)` by TDLAT_1:2; then reconsider A = LSeg(p,q) as Subset of (TOP-REAL 2)|(L~f)` by PRE_TOPC:8; LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1; then consider L being Subset of (TOP-REAL 2)|(L~f)` such that A3: L = LeftComp f and A4: L is a_component by CONNSP_1:def 6; q in A by RLTOPSP1:68; then A5: L meets A by A2,A3,XBOOLE_0:3; RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2; then consider R being Subset of (TOP-REAL 2)|(L~f)` such that A6: R = RightComp f and A7: R is a_component by CONNSP_1:def 6; p in A by RLTOPSP1:68; then A is connected & R meets A by A1,A6,CONNSP_1:23,XBOOLE_0:3; hence contradiction by A6,A7,A3,A4,A5,JORDAN2C:92,SPRECT_4:6; end; theorem Th28: Cl RightComp SpStSeq C = product((1,2)-->([.W-bound L~SpStSeq C, E-bound L~SpStSeq C.], [.S-bound L~SpStSeq C,N-bound L~SpStSeq C.])) proof set g = (1,2)-->([.W-bound L~SpStSeq C,E-bound L~SpStSeq C.], [.S-bound L~ SpStSeq C,N-bound L~SpStSeq C.]); A1: dom g = {1,2} by FUNCT_4:62; A2: Cl RightComp SpStSeq C = (RightComp SpStSeq C) \/ L~SpStSeq C by Th21; hereby let a be object; assume A3: a in Cl RightComp SpStSeq C; then reconsider b = a as Point of TOP-REAL 2; reconsider h = a as FinSequence by A3; A4: for x being object st x in {1,2} holds h.x in g.x proof let x be object such that A5: x in {1,2}; per cases by A5,TARSKI:def 2; suppose A6: x = 1; then A7: g.x = [.W-bound L~SpStSeq C,E-bound L~SpStSeq C.] by FUNCT_4:63; now per cases by A2,A3,XBOOLE_0:def 3; case a in RightComp SpStSeq C; then W-bound L~SpStSeq C < b`1 & E-bound L~SpStSeq C > b`1 by Th23 ,Th24; hence thesis by A6,A7,XXREAL_1:1; end; case a in L~SpStSeq C; then W-bound L~SpStSeq C <= b`1 & b`1 <= E-bound L~SpStSeq C by PSCOMP_1:24; hence thesis by A6,A7,XXREAL_1:1; end; end; hence thesis; end; suppose A8: x = 2; then A9: g.x = [.S-bound L~SpStSeq C,N-bound L~SpStSeq C.] by FUNCT_4:63; now per cases by A2,A3,XBOOLE_0:def 3; case a in RightComp SpStSeq C; then S-bound L~SpStSeq C < b`2 & N-bound L~SpStSeq C > b`2 by Th25 ,Th26; hence thesis by A8,A9,XXREAL_1:1; end; case a in L~SpStSeq C; then S-bound L~SpStSeq C <= b`2 & b`2 <= N-bound L~SpStSeq C by PSCOMP_1:24; hence thesis by A8,A9,XXREAL_1:1; end; end; hence thesis; end; end; a is Tuple of 2,REAL by A3,Lm1,FINSEQ_2:131; then ex r, s being Element of REAL st a = <*r,s*> by FINSEQ_2:100; then dom h = {1,2} by FINSEQ_1:2,89; hence a in product g by A1,A4,CARD_3:9; end; let a be object; assume a in product g; then consider h being Function such that A10: a = h and A11: dom h = dom g and A12: for x being object st x in dom g holds h.x in g.x by CARD_3:def 5; A13: [.S-bound L~SpStSeq C,N-bound L~SpStSeq C.] = {s where s is Real: S-bound L~SpStSeq C <= s & s <= N-bound L~SpStSeq C} by RCOMP_1:def 1; 2 in dom g by A1,TARSKI:def 2; then h.2 in g.2 by A12; then h.2 in [.S-bound L~SpStSeq C,N-bound L~SpStSeq C.] by FUNCT_4:63; then consider s being Real such that A14: h.2 = s and A15: S-bound L~SpStSeq C <= s & s <= N-bound L~SpStSeq C by A13; A16: [.W-bound L~SpStSeq C,E-bound L~SpStSeq C.] = {r where r is Real : W-bound L~SpStSeq C <= r & r <= E-bound L~SpStSeq C} by RCOMP_1:def 1; 1 in dom g by A1,TARSKI:def 2; then h.1 in g.1 by A12; then h.1 in [.W-bound L~SpStSeq C,E-bound L~SpStSeq C.] by FUNCT_4:63; then consider r being Real such that A17: h.1 = r and A18: W-bound L~SpStSeq C <= r & r <= E-bound L~SpStSeq C by A16; A19: LeftComp SpStSeq C = {q: not(W-bound L~SpStSeq C <= q`1 & q`1 <= E-bound L~SpStSeq C & S-bound L~SpStSeq C <= q`2 & q`2 <= N-bound L~SpStSeq C)} by SPRECT_3:37; A20: for k being object st k in dom h holds h.k = <*r,s*>.k proof let k be object; assume k in dom h; then k = 1 or k = 2 by A11,TARSKI:def 2; hence thesis by A17,A14,FINSEQ_1:44; end; dom <*r,s*> = {1,2} by FINSEQ_1:2,89; then A21: a = |[r,s]| by A10,A11,A20,FUNCT_1:2,FUNCT_4:62; assume not a in Cl RightComp SpStSeq C; then ( not a in RightComp SpStSeq C)& not a in L~SpStSeq C by A2, XBOOLE_0:def 3; then a in LeftComp SpStSeq C by A21,Th16; then ex q st q = a & not(W-bound L~SpStSeq C <= q`1 & q`1 <= E-bound L~ SpStSeq C & S-bound L~SpStSeq C <= q`2 & q`2 <= N-bound L~SpStSeq C) by A19; hence contradiction by A18,A15,A21,EUCLID:52; end; theorem Th29: proj1.:(Cl RightComp f) = proj1.:(L~f) proof set g = Rotate(f,N-min L~f); A1: L~f = L~g by REVROT_1:33; N-min L~f in rng f by SPRECT_2:39; then A2: g/.1 = N-min L~g by A1,FINSEQ_6:92; thus proj1.:(Cl RightComp f) c= proj1.:(L~f) proof A3: Cl RightComp f = (RightComp f) \/ L~f by Th21; let a be object; assume a in proj1.:(Cl RightComp f); then consider x being object such that A4: x in the carrier of TOP-REAL 2 and A5: x in Cl RightComp f and A6: a = proj1.x by FUNCT_2:64; per cases by A5,A3,XBOOLE_0:def 3; suppose A7: x in RightComp f; reconsider x as Point of TOP-REAL 2 by A4; set b = |[x`1,N-bound L~f + 1]|; b`2 = N-bound L~f + 1 & N-bound L~f + 1 > N-bound L~f + 0 by EUCLID:52 ,XREAL_1:6; then b in LeftComp g by A1,A2,JORDAN2C:113; then b in LeftComp f by REVROT_1:36; then LSeg(x,b) meets L~f by A7,Th27; then consider c being object such that A8: c in LSeg(x,b) and A9: c in L~f by XBOOLE_0:3; reconsider c as Point of TOP-REAL 2 by A8; A10: b`1 = x`1 by EUCLID:52; proj1.c = c`1 by PSCOMP_1:def 5 .= x`1 by A8,A10,GOBOARD7:5 .= a by A6,PSCOMP_1:def 5; hence thesis by A9,FUNCT_2:35; end; suppose x in L~f; hence thesis by A6,FUNCT_2:35; end; end; L~f = (Cl RightComp f) \ RightComp f by Th19; hence thesis by RELAT_1:123,XBOOLE_1:36; end; theorem Th30: proj2.:(Cl RightComp f) = proj2.:(L~f) proof set g = Rotate(f,N-min L~f); A1: L~f = L~g by REVROT_1:33; N-min L~f in rng f by SPRECT_2:39; then A2: g/.1 = N-min L~g by A1,FINSEQ_6:92; thus proj2.:(Cl RightComp f) c= proj2.:(L~f) proof A3: Cl RightComp f = (RightComp f) \/ L~f by Th21; let a be object; assume a in proj2.:(Cl RightComp f); then consider x being object such that A4: x in the carrier of TOP-REAL 2 and A5: x in Cl RightComp f and A6: a = proj2.x by FUNCT_2:64; per cases by A5,A3,XBOOLE_0:def 3; suppose A7: x in RightComp f; reconsider x as Point of TOP-REAL 2 by A4; set b = |[E-bound L~f + 1,x`2]|; b`1 = E-bound L~f + 1 & E-bound L~f + 1 > E-bound L~f + 0 by EUCLID:52 ,XREAL_1:6; then b in LeftComp g by A1,A2,JORDAN2C:111; then b in LeftComp f by REVROT_1:36; then LSeg(x,b) meets L~f by A7,Th27; then consider c be object such that A8: c in LSeg(x,b) and A9: c in L~f by XBOOLE_0:3; reconsider c as Point of TOP-REAL 2 by A8; A10: b`2 = x`2 by EUCLID:52; proj2.c = c`2 by PSCOMP_1:def 6 .= x`2 by A8,A10,GOBOARD7:6 .= a by A6,PSCOMP_1:def 6; hence thesis by A9,FUNCT_2:35; end; suppose x in L~f; hence thesis by A6,FUNCT_2:35; end; end; L~f = (Cl RightComp f) \ RightComp f by Th19; hence thesis by RELAT_1:123,XBOOLE_1:36; end; theorem Th31: RightComp g c= RightComp SpStSeq L~g proof let a be object; assume A1: a in RightComp g; then reconsider p = a as Point of TOP-REAL 2; p`1 > W-bound L~g by A1,Th23; then A2: p`1 > W-bound L~SpStSeq L~g by SPRECT_1:58; p`2 > S-bound L~g by A1,Th26; then A3: p`2 > S-bound L~SpStSeq L~g by SPRECT_1:59; p`1 < E-bound L~g by A1,Th24; then A4: p`1 < E-bound L~SpStSeq L~g by SPRECT_1:61; p`2 < N-bound L~g by A1,Th25; then A5: p`2 < N-bound L~SpStSeq L~g by SPRECT_1:60; RightComp SpStSeq L~g = {q : W-bound L~SpStSeq L~g < q`1 & q`1 < E-bound L~SpStSeq L~g & S-bound L~SpStSeq L~g < q`2 & q`2 < N-bound L~SpStSeq L~g} by SPRECT_3:37; hence thesis by A2,A4,A3,A5; end; theorem Th32: Cl RightComp g is compact proof Cl RightComp SpStSeq L~g = product((1,2)-->([.W-bound L~SpStSeq L~g, E-bound L~SpStSeq L~g.], [.S-bound L~SpStSeq L~g,N-bound L~SpStSeq L~g.])) by Th28; then A1: Cl RightComp SpStSeq L~g is compact by TOPREAL6:78; RightComp g c= RightComp SpStSeq L~g by Th31; hence thesis by A1,COMPTS_1:9,PRE_TOPC:19; end; theorem Th33: LeftComp g is non bounded proof Cl RightComp g is compact by Th32; then RightComp g is bounded by PRE_TOPC:18,RLTOPSP1:42; then A1: L~g \/ RightComp g is bounded by TOPREAL6:67; L~g \/ RightComp g \/ LeftComp g = the carrier of TOP-REAL 2 by Th15; hence thesis by A1,TOPREAL6:66; end; theorem Th34: LeftComp g is_outside_component_of L~g by GOBOARD9:def 1,Th33; theorem RightComp g is_inside_component_of L~g proof thus RightComp g is_a_component_of (L~g)` by GOBOARD9:def 2; Cl RightComp g is compact by Th32; hence thesis by PRE_TOPC:18,RLTOPSP1:42; end; theorem Th36: UBD L~g = LeftComp g proof UBD L~g is_outside_component_of L~g & LeftComp g is_outside_component_of L~g by Th34,JORDAN2C:68; hence thesis by JORDAN2C:119; end; theorem Th37: BDD L~g = RightComp g proof A1: (BDD L~g) misses (UBD L~g) by JORDAN2C:24; A2: (L~g)` = (BDD L~g) \/ (UBD L~g) & LeftComp g misses RightComp g by Th14, JORDAN2C:27; UBD L~g = LeftComp g & (L~g)` = LeftComp g \/ RightComp g by Th36,GOBRD12:10; hence thesis by A2,A1,XBOOLE_1:71; end; theorem P is_outside_component_of L~g implies P = LeftComp g proof assume A1: P is_outside_component_of L~g; UBD L~g is_outside_component_of L~g by JORDAN2C:68; then P = UBD L~g by A1,JORDAN2C:119; hence thesis by Th36; end; theorem Th39: P is_inside_component_of L~g implies P meets RightComp g proof assume P is_inside_component_of L~g; then A1: P c= BDD L~g & P is_a_component_of (L~g)` by JORDAN2C:22; BDD L~g = RightComp g by Th37; hence thesis by A1,SPRECT_1:4,XBOOLE_1:67; end; theorem P is_inside_component_of L~g implies P = BDD L~g proof A1: RightComp g = BDD L~g by Th37; BDD L~g is_inside_component_of L~g by JORDAN2C:108; then A2: BDD L~g is_a_component_of (L~g)`; assume A3: P is_inside_component_of L~g; thus thesis by A3,A1,A2,Th39,GOBOARD9:1; end; theorem W-bound L~g = W-bound RightComp g proof set A = (Cl RightComp g) \ RightComp g; A1: W-bound Cl RightComp g = lower_bound (proj1.:(Cl RightComp g)) by SPRECT_1:43; A2: L~g = A by Th19; Cl RightComp g is compact by Th32; then A3: RightComp g is bounded by PRE_TOPC:18,RLTOPSP1:42; reconsider A as non empty Subset of TOP-REAL 2 by A2; proj1.:(Cl RightComp g) = proj1.:(L~g) & W-bound A = lower_bound (proj1 .:A) by Th29,SPRECT_1:43; hence thesis by A2,A3,A1,TOPREAL6:85; end; theorem E-bound L~g = E-bound RightComp g proof set A = (Cl RightComp g) \ RightComp g; A1: E-bound Cl RightComp g = upper_bound (proj1.:(Cl RightComp g)) by SPRECT_1:46; A2: L~g = A by Th19; Cl RightComp g is compact by Th32; then A3: RightComp g is bounded by PRE_TOPC:18,RLTOPSP1:42; reconsider A as non empty Subset of TOP-REAL 2 by A2; proj1.:(Cl RightComp g) = proj1.:(L~g) & E-bound A = upper_bound (proj1.:A) by Th29,SPRECT_1:46; hence thesis by A2,A3,A1,TOPREAL6:86; end; theorem N-bound L~g = N-bound RightComp g proof set A = (Cl RightComp g) \ RightComp g; A1: N-bound Cl RightComp g = upper_bound (proj2.:(Cl RightComp g)) by SPRECT_1:45; A2: L~g = A by Th19; Cl RightComp g is compact by Th32; then A3: RightComp g is bounded by PRE_TOPC:18,RLTOPSP1:42; reconsider A as non empty Subset of TOP-REAL 2 by A2; proj2.:(Cl RightComp g) = proj2.:(L~g) & N-bound A = upper_bound (proj2.:A) by Th30,SPRECT_1:45; hence thesis by A2,A3,A1,TOPREAL6:87; end; theorem S-bound L~g = S-bound RightComp g proof set A = (Cl RightComp g) \ RightComp g; A1: S-bound Cl RightComp g = lower_bound (proj2.:(Cl RightComp g)) by SPRECT_1:44; A2: L~g = A by Th19; Cl RightComp g is compact by Th32; then A3: RightComp g is bounded by PRE_TOPC:18,RLTOPSP1:42; reconsider A as non empty Subset of TOP-REAL 2 by A2; proj2.:(Cl RightComp g) = proj2.:(L~g) & S-bound A = lower_bound (proj2 .:A) by Th30,SPRECT_1:44; hence thesis by A2,A3,A1,TOPREAL6:88; end;