:: GOBRD14 semantic presentation begin Lm1: the carrier of (TOP-REAL 2) = REAL 2 by EUCLID:22; theorem :: GOBRD14:1 for f being non constant standard special_circular_sequence for P being Subset of (TOP-REAL 2) for p being Point of (Euclid 2) st p = 0.REAL 2 & P is_outside_component_of L~ f holds ex r being Real st ( r > 0 & (Ball (p,r)) ` c= P ) proof let f be non constant standard special_circular_sequence; ::_thesis: for P being Subset of (TOP-REAL 2) for p being Point of (Euclid 2) st p = 0.REAL 2 & P is_outside_component_of L~ f holds ex r being Real st ( r > 0 & (Ball (p,r)) ` c= P ) let P be Subset of (TOP-REAL 2); ::_thesis: for p being Point of (Euclid 2) st p = 0.REAL 2 & P is_outside_component_of L~ f holds ex r being Real st ( r > 0 & (Ball (p,r)) ` c= P ) let p be Point of (Euclid 2); ::_thesis: ( p = 0.REAL 2 & P is_outside_component_of L~ f implies ex r being Real st ( r > 0 & (Ball (p,r)) ` c= P ) ) assume that A1: p = 0.REAL 2 and A2: P is_outside_component_of L~ f ; ::_thesis: ex r being Real st ( r > 0 & (Ball (p,r)) ` c= P ) 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 ((dist (p,c)) + r) + 1 ; ::_thesis: ( ((dist (p,c)) + r) + 1 > 0 & (Ball (p,(((dist (p,c)) + r) + 1))) ` c= P ) set L = (REAL 2) \ { a where a is Point of (TOP-REAL 2) : |.a.| < ((dist (p,c)) + r) + 1 } ; ((dist (p,c)) + r) + 0 < ((dist (p,c)) + r) + 1 by XREAL_1:8; hence 0 < ((dist (p,c)) + r) + 1 by A3, METRIC_1:5, XREAL_1:8; ::_thesis: (Ball (p,(((dist (p,c)) + r) + 1))) ` c= P then ((dist (p,c)) + r) + 1 = abs (((dist (p,c)) + r) + 1) by ABSVALUE:def_1; then for a being Point of (TOP-REAL 2) holds ( a <> |[0,(((dist (p,c)) + r) + 1)]| or |.a.| >= ((dist (p,c)) + r) + 1 ) by TOPREAL6:23; then not |[0,(((dist (p,c)) + r) + 1)]| in { a where a is Point of (TOP-REAL 2) : |.a.| < ((dist (p,c)) + r) + 1 } ; then reconsider L = (REAL 2) \ { a where a is Point of (TOP-REAL 2) : |.a.| < ((dist (p,c)) + r) + 1 } as non empty Subset of (TOP-REAL 2) by Lm1, XBOOLE_0:def_5; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Ball (p,(((dist (p,c)) + r) + 1))) ` or x in P ) assume A5: x in (Ball (p,(((dist (p,c)) + r) + 1))) ` ; ::_thesis: x in P 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,(((dist (p,c)) + r) + 1)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in Ball (p,(((dist (p,c)) + r) + 1)) ) A8: ((dist (p,c)) + r) + 0 < ((dist (p,c)) + r) + 1 by XREAL_1:6; assume A9: x in D ; ::_thesis: x in Ball (p,(((dist (p,c)) + r) + 1)) 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 x in Ball (p,(((dist (p,c)) + r) + 1)) by METRIC_1:11; ::_thesis: verum end; A11: L c= (L~ f) ` proof let l be set ; :: according to TARSKI:def_3 ::_thesis: ( not l in L or l in (L~ f) ` ) assume A12: l in L ; ::_thesis: l in (L~ f) ` 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.| < ((dist (p,c)) + r) + 1 } by A12, XBOOLE_0:def_5; then A13: |.j.| >= ((dist (p,c)) + r) + 1 ; now__::_thesis:_not_l_in_L~_f assume l in L~ f ; ::_thesis: contradiction then dist (t,p) < ((dist (p,c)) + r) + 1 by A7, METRIC_1:11; hence contradiction by A1, A13, TOPREAL6:25; ::_thesis: verum end; hence l in (L~ f) ` by A12, SUBSET_1:29; ::_thesis: verum 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; :: according to JORDAN2C:def_3 ::_thesis: not M is bounded not W is bounded by JORDAN2C:62; then not L is bounded by JORDAN2C:11; hence not M is bounded by A15, RLTOPSP1:42; ::_thesis: verum 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,(((dist (p,c)) + r) + 1)) by A5, XBOOLE_0:def_5; then for k being Point of (TOP-REAL 2) holds ( k <> z or |.k.| >= ((dist (p,c)) + r) + 1 ) by A6, METRIC_1:11; then ( z in REAL 2 & not x in { a where a is Point of (TOP-REAL 2) : |.a.| < ((dist (p,c)) + r) + 1 } ) ; 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 x in P by A17, A15, A16, TARSKI:def_4; ::_thesis: verum end; begin theorem :: GOBRD14:2 for n being Element of NAT for f being FinSequence of (TOP-REAL n) st L~ f <> {} holds 2 <= len f proof let n be Element of NAT ; ::_thesis: for f being FinSequence of (TOP-REAL n) st L~ f <> {} holds 2 <= len f let f be FinSequence of (TOP-REAL n); ::_thesis: ( L~ f <> {} implies 2 <= len f ) assume L~ f <> {} ; ::_thesis: 2 <= len 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 2 <= len f ; ::_thesis: verum end; theorem Th3: :: GOBRD14:3 for i, j being Element of NAT for G being Go-board st 1 <= i & i < len G & 1 <= j & j < width G holds 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 let i, j be Element of NAT ; ::_thesis: for G being Go-board st 1 <= i & i < len G & 1 <= j & j < width G holds 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).])) let G be Go-board; ::_thesis: ( 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).])) ) 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 ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) = {1,2} by FUNCT_4:62; assume ( 1 <= i & i < len G & 1 <= j & j < width G ) ; ::_thesis: 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).])) 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 ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) :: according to XBOOLE_0:def_10 ::_thesis: product ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) c= cell (G,i,j) proof let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in cell (G,i,j) or c in product ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) ) assume c in cell (G,i,j) ; ::_thesis: c in product ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) 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 set st x in dom ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) holds <*r,s*> . x in ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) . x proof let x be set ; ::_thesis: ( x in dom ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) implies <*r,s*> . x in ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) . x ) A9: s = |[r,s]| `2 by EUCLID:52 .= <*r,s*> . 2 ; assume x in dom ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) ; ::_thesis: <*r,s*> . x in ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) . x then A10: ( x = 1 or x = 2 ) by TARSKI:def_2; r = |[r,s]| `1 by EUCLID:52 .= <*r,s*> . 1 ; hence <*r,s*> . x in ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) . x by A7, A10, A9, FUNCT_4:63; ::_thesis: verum end; dom <*r,s*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89; hence c in product ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) by A2, A5, A8, CARD_3:9; ::_thesis: verum end; let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in product ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) or c in cell (G,i,j) ) assume c in product ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) ; ::_thesis: c in cell (G,i,j) then consider g being Function such that A11: c = g and A12: dom g = dom ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) and A13: for x being set st x in dom ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) holds g . x in ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) . x by CARD_3:def_5; 2 in dom ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) by A2, TARSKI:def_2; then g . 2 in ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) . 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 ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) by A2, TARSKI:def_2; then g . 1 in ((1,2) --> ([.((G * (i,1)) `1),((G * ((i + 1),1)) `1).],[.((G * (1,j)) `2),((G * (1,(j + 1))) `2).])) . 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 set st k in dom g holds g . k = <*a,b*> . k proof let k be set ; ::_thesis: ( k in dom g implies g . k = <*a,b*> . k ) assume k in dom g ; ::_thesis: g . k = <*a,b*> . k then ( k = 1 or k = 2 ) by A12, TARSKI:def_2; hence g . k = <*a,b*> . k by A16, A14, FINSEQ_1:44; ::_thesis: verum end; dom <*a,b*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89; then c = |[a,b]| by A11, A12, A18, FUNCT_1:2, FUNCT_4:62; hence c in cell (G,i,j) by A3, A17, A15; ::_thesis: verum end; theorem :: GOBRD14:4 for i, j being Element of NAT for G being Go-board st 1 <= i & i < len G & 1 <= j & j < width G holds cell (G,i,j) is compact proof let i, j be Element of NAT ; ::_thesis: for G being Go-board st 1 <= i & i < len G & 1 <= j & j < width G holds cell (G,i,j) is compact let G be Go-board; ::_thesis: ( 1 <= i & i < len G & 1 <= j & j < width G implies cell (G,i,j) is compact ) assume ( 1 <= i & i < len G & 1 <= j & j < width G ) ; ::_thesis: cell (G,i,j) is compact 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 cell (G,i,j) is compact by TOPREAL6:78; ::_thesis: verum end; theorem :: GOBRD14:5 for i, j, n being Element of NAT for G being Go-board st [i,j] in Indices G & [(i + n),j] in Indices G holds dist ((G * (i,j)),(G * ((i + n),j))) = ((G * ((i + n),j)) `1) - ((G * (i,j)) `1) proof let i, j, n be Element of NAT ; ::_thesis: for G being Go-board st [i,j] in Indices G & [(i + n),j] in Indices G holds dist ((G * (i,j)),(G * ((i + n),j))) = ((G * ((i + n),j)) `1) - ((G * (i,j)) `1) let G be Go-board; ::_thesis: ( [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) ) assume that A1: [i,j] in Indices G and A2: [(i + n),j] in Indices G ; ::_thesis: dist ((G * (i,j)),(G * ((i + n),j))) = ((G * ((i + n),j)) `1) - ((G * (i,j)) `1) set x = G * (i,j); set y = G * ((i + n),j); percases ( n = 0 or n <> 0 ) ; suppose n = 0 ; ::_thesis: dist ((G * (i,j)),(G * ((i + n),j))) = ((G * ((i + n),j)) `1) - ((G * (i,j)) `1) hence dist ((G * (i,j)),(G * ((i + n),j))) = ((G * ((i + n),j)) `1) - ((G * (i,j)) `1) by TOPREAL6:93; ::_thesis: verum end; supposeA3: n <> 0 ; ::_thesis: dist ((G * (i,j)),(G * ((i + n),j))) = ((G * ((i + n),j)) `1) - ((G * (i,j)) `1) A4: i + n <= len G by A2, MATRIX_1:38; A5: 1 <= i by A1, MATRIX_1:38; A6: 1 <= i + n by A2, MATRIX_1:38; A7: ( 1 <= j & j <= width G ) by A1, MATRIX_1:38; 1 <= n by A3, NAT_1:14; then i < i + n by NAT_1:19; then (G * (i,j)) `1 < (G * ((i + n),j)) `1 by A4, A7, A5, GOBOARD5:3; then A8: ((G * (i,j)) `1) - ((G * (i,j)) `1) < ((G * ((i + n),j)) `1) - ((G * (i,j)) `1) by XREAL_1:14; i <= len G by A1, MATRIX_1:38; then A9: (G * (i,j)) `2 = (G * (1,j)) `2 by A7, A5, GOBOARD5:1 .= (G * ((i + n),j)) `2 by A6, A4, A7, GOBOARD5:1 ; thus dist ((G * (i,j)),(G * ((i + n),j))) = sqrt (((((G * (i,j)) `1) - ((G * ((i + n),j)) `1)) ^2) + ((((G * (i,j)) `2) - ((G * ((i + n),j)) `2)) ^2)) by TOPREAL6:92 .= abs (((G * (i,j)) `1) - ((G * ((i + n),j)) `1)) by A9, COMPLEX1:72 .= abs (- (((G * (i,j)) `1) - ((G * ((i + n),j)) `1))) by COMPLEX1:52 .= ((G * ((i + n),j)) `1) - ((G * (i,j)) `1) by A8, ABSVALUE:def_1 ; ::_thesis: verum end; end; end; theorem :: GOBRD14:6 for i, j, n being Element of NAT for G being Go-board st [i,j] in Indices G & [i,(j + n)] in Indices G holds dist ((G * (i,j)),(G * (i,(j + n)))) = ((G * (i,(j + n))) `2) - ((G * (i,j)) `2) proof let i, j, n be Element of NAT ; ::_thesis: for G being Go-board st [i,j] in Indices G & [i,(j + n)] in Indices G holds dist ((G * (i,j)),(G * (i,(j + n)))) = ((G * (i,(j + n))) `2) - ((G * (i,j)) `2) let G be Go-board; ::_thesis: ( [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) ) assume that A1: [i,j] in Indices G and A2: [i,(j + n)] in Indices G ; ::_thesis: dist ((G * (i,j)),(G * (i,(j + n)))) = ((G * (i,(j + n))) `2) - ((G * (i,j)) `2) set x = G * (i,j); set y = G * (i,(j + n)); percases ( n = 0 or n <> 0 ) ; suppose n = 0 ; ::_thesis: dist ((G * (i,j)),(G * (i,(j + n)))) = ((G * (i,(j + n))) `2) - ((G * (i,j)) `2) hence dist ((G * (i,j)),(G * (i,(j + n)))) = ((G * (i,(j + n))) `2) - ((G * (i,j)) `2) by TOPREAL6:93; ::_thesis: verum end; supposeA3: n <> 0 ; ::_thesis: dist ((G * (i,j)),(G * (i,(j + n)))) = ((G * (i,(j + n))) `2) - ((G * (i,j)) `2) A4: j + n <= width G by A2, MATRIX_1:38; A5: ( 1 <= i & i <= len G ) by A1, MATRIX_1:38; A6: 1 <= j + n by A2, MATRIX_1:38; A7: 1 <= j by A1, MATRIX_1:38; 1 <= n by A3, NAT_1:14; then j < j + n by NAT_1:19; then (G * (i,j)) `2 < (G * (i,(j + n))) `2 by A4, A7, A5, GOBOARD5:4; then A8: ((G * (i,j)) `2) - ((G * (i,j)) `2) < ((G * (i,(j + n))) `2) - ((G * (i,j)) `2) by XREAL_1:14; j <= width G by A1, MATRIX_1:38; then A9: (G * (i,j)) `1 = (G * (i,1)) `1 by A7, A5, GOBOARD5:2 .= (G * (i,(j + n))) `1 by A6, A4, A5, GOBOARD5:2 ; thus dist ((G * (i,j)),(G * (i,(j + n)))) = sqrt (((((G * (i,j)) `1) - ((G * (i,(j + n))) `1)) ^2) + ((((G * (i,j)) `2) - ((G * (i,(j + n))) `2)) ^2)) by TOPREAL6:92 .= abs (((G * (i,j)) `2) - ((G * (i,(j + n))) `2)) by A9, COMPLEX1:72 .= abs (- (((G * (i,j)) `2) - ((G * (i,(j + n))) `2))) by COMPLEX1:52 .= ((G * (i,(j + n))) `2) - ((G * (i,j)) `2) by A8, ABSVALUE:def_1 ; ::_thesis: verum end; end; end; theorem :: GOBRD14:7 for n being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds 3 <= (len (Gauge (C,n))) -' 1 proof let n be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds 3 <= (len (Gauge (C,n))) -' 1 let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: 3 <= (len (Gauge (C,n))) -' 1 set G = Gauge (C,n); 4 <= len (Gauge (C,n)) by JORDAN8:10; then 4 - 1 <= (len (Gauge (C,n))) - 1 by XREAL_1:13; hence 3 <= (len (Gauge (C,n))) -' 1 by XREAL_0:def_2; ::_thesis: verum end; theorem :: GOBRD14:8 for i, j being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st i <= j holds for a, b being Element of NAT st 2 <= a & a <= (len (Gauge (C,i))) - 1 & 2 <= b & b <= (len (Gauge (C,i))) - 1 holds ex c, d being Element of 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 let i, j be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st i <= j holds for a, b being Element of NAT st 2 <= a & a <= (len (Gauge (C,i))) - 1 & 2 <= b & b <= (len (Gauge (C,i))) - 1 holds ex c, d being Element of 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)) ) let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( i <= j implies for a, b being Element of NAT st 2 <= a & a <= (len (Gauge (C,i))) - 1 & 2 <= b & b <= (len (Gauge (C,i))) - 1 holds ex c, d being Element of 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)) ) ) A1: 0 <> 2 |^ i by NEWTON:83; assume A2: i <= j ; ::_thesis: for a, b being Element of NAT st 2 <= a & a <= (len (Gauge (C,i))) - 1 & 2 <= b & b <= (len (Gauge (C,i))) - 1 holds ex c, d being Element of 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)) ) 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 Element of NAT ; ::_thesis: ( 2 <= a & a <= (len (Gauge (C,i))) - 1 & 2 <= b & b <= (len (Gauge (C,i))) - 1 implies ex c, d being Element of 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)) ) ) assume that A4: 2 <= a and A5: a <= (len (Gauge (C,i))) - 1 and A6: 2 <= b and A7: b <= (len (Gauge (C,i))) - 1 ; ::_thesis: ex c, d being Element of 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)) ) A8: ( 1 <= a & 1 <= b ) by A4, A6, XXREAL_0:2; set c = 2 + ((2 |^ (j -' i)) * (a -' 2)); set d = 2 + ((2 |^ (j -' i)) * (b -' 2)); A9: 0 <= b - 2 by A6, XREAL_1:48; set n = N-bound C; set e = E-bound C; set s = S-bound C; set w = W-bound C; A10: 0 <> 2 |^ j by NEWTON:83; A11: (((N-bound C) - (S-bound C)) / (2 |^ j)) * ((2 + ((2 |^ (j -' i)) * (b -' 2))) - 2) = (((N-bound C) - (S-bound C)) / (2 |^ j)) * (((2 |^ j) / (2 |^ i)) * (b -' 2)) by A2, TOPREAL6:10 .= ((((N-bound C) - (S-bound C)) / (2 |^ j)) * ((2 |^ j) / (2 |^ i))) * (b -' 2) .= (((N-bound C) - (S-bound C)) / ((2 |^ j) / ((2 |^ j) / (2 |^ i)))) * (b -' 2) by XCMPLX_1:81 .= (((N-bound C) - (S-bound C)) / (2 |^ i)) * (b -' 2) by A10, XCMPLX_1:52 .= (((N-bound C) - (S-bound C)) / (2 |^ i)) * (b - 2) by A9, XREAL_0:def_2 ; take 2 + ((2 |^ (j -' i)) * (a -' 2)) ; ::_thesis: ex d being Element of NAT st ( 2 <= 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (a -' 2)) <= (len (Gauge (C,j))) - 1 & 2 <= d & d <= (len (Gauge (C,j))) - 1 & [(2 + ((2 |^ (j -' i)) * (a -' 2))),d] in Indices (Gauge (C,j)) & (Gauge (C,i)) * (a,b) = (Gauge (C,j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))),d) & 2 + ((2 |^ (j -' i)) * (a -' 2)) = 2 + ((2 |^ (j -' i)) * (a -' 2)) & d = 2 + ((2 |^ (j -' i)) * (b -' 2)) ) take 2 + ((2 |^ (j -' i)) * (b -' 2)) ; ::_thesis: ( 2 <= 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (a -' 2)) <= (len (Gauge (C,j))) - 1 & 2 <= 2 + ((2 |^ (j -' i)) * (b -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) <= (len (Gauge (C,j))) - 1 & [(2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))] in Indices (Gauge (C,j)) & (Gauge (C,i)) * (a,b) = (Gauge (C,j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))) & 2 + ((2 |^ (j -' i)) * (a -' 2)) = 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) = 2 + ((2 |^ (j -' i)) * (b -' 2)) ) A12: 2 + 0 <= 2 + ((2 |^ (j -' i)) * (a -' 2)) by XREAL_1:6; then A13: 1 <= 2 + ((2 |^ (j -' i)) * (a -' 2)) 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-bound C) - (W-bound C)) / (2 |^ j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))) - 2) = (((E-bound C) - (W-bound C)) / (2 |^ j)) * (((2 |^ j) / (2 |^ i)) * (a -' 2)) by A2, TOPREAL6:10 .= ((((E-bound C) - (W-bound C)) / (2 |^ j)) * ((2 |^ j) / (2 |^ i))) * (a -' 2) .= (((E-bound C) - (W-bound C)) / ((2 |^ j) / ((2 |^ j) / (2 |^ i)))) * (a -' 2) by XCMPLX_1:81 .= (((E-bound C) - (W-bound C)) / (2 |^ i)) * (a -' 2) by A10, XCMPLX_1:52 .= (((E-bound C) - (W-bound C)) / (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 <= 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (a -' 2)) <= (len (Gauge (C,j))) - 1 & 2 <= 2 + ((2 |^ (j -' i)) * (b -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) <= (len (Gauge (C,j))) - 1 ) by A19, A20, A12, XREAL_1:6; ::_thesis: ( [(2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))] in Indices (Gauge (C,j)) & (Gauge (C,i)) * (a,b) = (Gauge (C,j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))) & 2 + ((2 |^ (j -' i)) * (a -' 2)) = 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) = 2 + ((2 |^ (j -' i)) * (b -' 2)) ) then A24: 1 <= 2 + ((2 |^ (j -' i)) * (b -' 2)) by XXREAL_0:2; width (Gauge (C,j)) = len (Gauge (C,j)) by JORDAN8:def_1; then A25: 2 + ((2 |^ (j -' i)) * (b -' 2)) <= width (Gauge (C,j)) by A23, A17, XXREAL_0:2; 2 + ((2 |^ (j -' i)) * (a -' 2)) <= len (Gauge (C,j)) by A23, A17, XXREAL_0:2; hence [(2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))] in Indices (Gauge (C,j)) by A13, A24, A25, MATRIX_1:36; ::_thesis: ( (Gauge (C,i)) * (a,b) = (Gauge (C,j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))) & 2 + ((2 |^ (j -' i)) * (a -' 2)) = 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) = 2 + ((2 |^ (j -' i)) * (b -' 2)) ) then A26: (Gauge (C,j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))) - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ j)) * ((2 + ((2 |^ (j -' i)) * (b -' 2))) - 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_1:36; then A27: (Gauge (C,i)) * (a,b) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ i)) * (a - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ i)) * (b - 2)))]| by JORDAN8:def_1; then A28: ((Gauge (C,i)) * (a,b)) `2 = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ i)) * (b - 2)) by EUCLID:52 .= ((Gauge (C,j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2))))) `2 by A26, A11, EUCLID:52 ; ((Gauge (C,i)) * (a,b)) `1 = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ i)) * (a - 2)) by A27, EUCLID:52 .= ((Gauge (C,j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2))))) `1 by A26, A16, EUCLID:52 ; hence (Gauge (C,i)) * (a,b) = (Gauge (C,j)) * ((2 + ((2 |^ (j -' i)) * (a -' 2))),(2 + ((2 |^ (j -' i)) * (b -' 2)))) by A28, TOPREAL3:6; ::_thesis: ( 2 + ((2 |^ (j -' i)) * (a -' 2)) = 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) = 2 + ((2 |^ (j -' i)) * (b -' 2)) ) thus ( 2 + ((2 |^ (j -' i)) * (a -' 2)) = 2 + ((2 |^ (j -' i)) * (a -' 2)) & 2 + ((2 |^ (j -' i)) * (b -' 2)) = 2 + ((2 |^ (j -' i)) * (b -' 2)) ) ; ::_thesis: verum end; theorem Th9: :: GOBRD14:9 for i, j, n being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st [i,j] in Indices (Gauge (C,n)) & [i,(j + 1)] in Indices (Gauge (C,n)) holds dist (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,(j + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ n) proof let i, j, n be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st [i,j] in Indices (Gauge (C,n)) & [i,(j + 1)] in Indices (Gauge (C,n)) holds dist (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,(j + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ n) let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( [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) ) set G = Gauge (C,n); set a = N-bound C; set e = E-bound C; set s = S-bound C; set w = W-bound C; set p1 = (Gauge (C,n)) * (i,j); set p2 = (Gauge (C,n)) * (i,(j + 1)); assume that A1: [i,j] in Indices (Gauge (C,n)) and A2: [i,(j + 1)] in Indices (Gauge (C,n)) ; ::_thesis: dist (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,(j + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ n) A3: (Gauge (C,n)) * (i,(j + 1)) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((j + 1) - 2)))]| by A2, JORDAN8:def_1; N-bound C >= S-bound C by SPRECT_1:22; then A4: (N-bound C) - (S-bound C) >= (S-bound C) - (S-bound C) by XREAL_1:9; set x = ((N-bound C) - (S-bound C)) / (2 |^ n); consider p, q being Point of (Euclid 2) such that A5: ( p = (Gauge (C,n)) * (i,j) & q = (Gauge (C,n)) * (i,(j + 1)) ) and A6: dist (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,(j + 1)))) = dist (p,q) by TOPREAL6:def_1; A7: (Gauge (C,n)) * (i,j) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| by A1, JORDAN8:def_1; dist (p,q) = (Pitag_dist 2) . (p,q) by METRIC_1:def_1 .= sqrt ((((((Gauge (C,n)) * (i,j)) `1) - (((Gauge (C,n)) * (i,(j + 1))) `1)) ^2) + (((((Gauge (C,n)) * (i,j)) `2) - (((Gauge (C,n)) * (i,(j + 1))) `2)) ^2)) by A5, TOPREAL3:7 .= sqrt (((((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))) - (((Gauge (C,n)) * (i,(j + 1))) `1)) ^2) + (((((Gauge (C,n)) * (i,j)) `2) - (((Gauge (C,n)) * (i,(j + 1))) `2)) ^2)) by A7, EUCLID:52 .= sqrt (((((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))) - ((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2)))) ^2) + (((((Gauge (C,n)) * (i,j)) `2) - (((Gauge (C,n)) * (i,(j + 1))) `2)) ^2)) by A3, EUCLID:52 .= abs ((((Gauge (C,n)) * (i,j)) `2) - (((Gauge (C,n)) * (i,(j + 1))) `2)) by COMPLEX1:72 .= abs (((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2))) - (((Gauge (C,n)) * (i,(j + 1))) `2)) by A7, EUCLID:52 .= abs (((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2))) - ((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((j + 1) - 2)))) by A3, EUCLID:52 .= abs (- (((N-bound C) - (S-bound C)) / (2 |^ n))) .= abs (((N-bound C) - (S-bound C)) / (2 |^ n)) by COMPLEX1:52 .= (abs ((N-bound C) - (S-bound C))) / (abs (2 |^ n)) by COMPLEX1:67 .= ((N-bound C) - (S-bound C)) / (abs (2 |^ n)) by A4, ABSVALUE:def_1 ; hence dist (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,(j + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ n) by A6, ABSVALUE:def_1; ::_thesis: verum end; theorem Th10: :: GOBRD14:10 for i, j, n being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st [i,j] in Indices (Gauge (C,n)) & [(i + 1),j] in Indices (Gauge (C,n)) holds dist (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * ((i + 1),j))) = ((E-bound C) - (W-bound C)) / (2 |^ n) proof let i, j, n be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st [i,j] in Indices (Gauge (C,n)) & [(i + 1),j] in Indices (Gauge (C,n)) holds dist (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * ((i + 1),j))) = ((E-bound C) - (W-bound C)) / (2 |^ n) let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( [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) ) set G = Gauge (C,n); set a = N-bound C; set e = E-bound C; set s = S-bound C; set w = W-bound C; set p1 = (Gauge (C,n)) * (i,j); set p2 = (Gauge (C,n)) * ((i + 1),j); assume that A1: [i,j] in Indices (Gauge (C,n)) and A2: [(i + 1),j] in Indices (Gauge (C,n)) ; ::_thesis: dist (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * ((i + 1),j))) = ((E-bound C) - (W-bound C)) / (2 |^ n) A3: (Gauge (C,n)) * ((i + 1),j) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * ((i + 1) - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| by A2, JORDAN8:def_1; E-bound C >= W-bound C by SPRECT_1:21; then A4: (E-bound C) - (W-bound C) >= (W-bound C) - (W-bound C) by XREAL_1:9; set x = ((E-bound C) - (W-bound C)) / (2 |^ n); consider p, q being Point of (Euclid 2) such that A5: ( p = (Gauge (C,n)) * (i,j) & q = (Gauge (C,n)) * ((i + 1),j) ) and A6: dist (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * ((i + 1),j))) = dist (p,q) by TOPREAL6:def_1; A7: (Gauge (C,n)) * (i,j) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| by A1, JORDAN8:def_1; dist (p,q) = (Pitag_dist 2) . (p,q) by METRIC_1:def_1 .= sqrt ((((((Gauge (C,n)) * (i,j)) `1) - (((Gauge (C,n)) * ((i + 1),j)) `1)) ^2) + (((((Gauge (C,n)) * (i,j)) `2) - (((Gauge (C,n)) * ((i + 1),j)) `2)) ^2)) by A5, TOPREAL3:7 .= sqrt ((((((Gauge (C,n)) * (i,j)) `1) - (((Gauge (C,n)) * ((i + 1),j)) `1)) ^2) + ((((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2))) - (((Gauge (C,n)) * ((i + 1),j)) `2)) ^2)) by A7, EUCLID:52 .= sqrt ((((((Gauge (C,n)) * (i,j)) `1) - (((Gauge (C,n)) * ((i + 1),j)) `1)) ^2) + ((((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2))) - ((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))) ^2)) by A3, EUCLID:52 .= abs ((((Gauge (C,n)) * (i,j)) `1) - (((Gauge (C,n)) * ((i + 1),j)) `1)) by COMPLEX1:72 .= abs (((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))) - (((Gauge (C,n)) * ((i + 1),j)) `1)) by A7, EUCLID:52 .= abs (((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))) - ((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * ((i + 1) - 2)))) by A3, EUCLID:52 .= abs (- (((E-bound C) - (W-bound C)) / (2 |^ n))) .= abs (((E-bound C) - (W-bound C)) / (2 |^ n)) by COMPLEX1:52 .= (abs ((E-bound C) - (W-bound C))) / (abs (2 |^ n)) by COMPLEX1:67 .= ((E-bound C) - (W-bound C)) / (abs (2 |^ n)) by A4, ABSVALUE:def_1 ; hence dist (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * ((i + 1),j))) = ((E-bound C) - (W-bound C)) / (2 |^ n) by A6, ABSVALUE:def_1; ::_thesis: verum end; theorem :: GOBRD14:11 for C being compact non horizontal non vertical Subset of (TOP-REAL 2) for r, t being real number st r > 0 & t > 0 holds ex n being Element of 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 C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for r, t being real number st r > 0 & t > 0 holds ex n being Element of 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 ) let r, t be real number ; ::_thesis: ( r > 0 & t > 0 implies ex n being Element of 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 ) ) assume that A1: r > 0 and A2: t > 0 ; ::_thesis: ex n being Element of 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 ) set n = N-bound C; set e = E-bound C; set s = S-bound C; set w = W-bound C; set a = (abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1; set b = (abs [\(log (2,(((E-bound C) - (W-bound C)) / t)))/]) + 1; take i = (max (((abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1),((abs [\(log (2,(((E-bound C) - (W-bound C)) / t)))/]) + 1))) + 1; ::_thesis: ( 1 < i & dist (((Gauge (C,i)) * (1,1)),((Gauge (C,i)) * (1,2))) < r & dist (((Gauge (C,i)) * (1,1)),((Gauge (C,i)) * (2,1))) < t ) A3: 2 to_power i > 0 by POWER:34; then A4: 2 |^ i > 0 by POWER:41; [\(log (2,(((N-bound C) - (S-bound C)) / r)))/] <= abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/] by ABSVALUE:4; then A5: [\(log (2,(((N-bound C) - (S-bound C)) / r)))/] + 1 <= (abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1 by XREAL_1:6; [\(log (2,(((N-bound C) - (S-bound C)) / r)))/] > (log (2,(((N-bound C) - (S-bound C)) / r))) - 1 by INT_1:def_6; then [\(log (2,(((N-bound C) - (S-bound C)) / r)))/] + 1 > ((log (2,(((N-bound C) - (S-bound C)) / r))) - 1) + 1 by XREAL_1:6; then A6: (abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1 > ((log (2,(((N-bound C) - (S-bound C)) / r))) - 1) + 1 by A5, XXREAL_0:2; (abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1 <= max (((abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1),((abs [\(log (2,(((E-bound C) - (W-bound C)) / t)))/]) + 1)) by XXREAL_0:25; then A7: ((abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1) + 1 <= (max (((abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1),((abs [\(log (2,(((E-bound C) - (W-bound C)) / t)))/]) + 1))) + 1 by XREAL_1:6; (abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1 < ((abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1) + 1 by XREAL_1:29; then i > (abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1 by A7, XXREAL_0:2; then i > log (2,(((N-bound C) - (S-bound C)) / r)) by A6, XXREAL_0:2; then log (2,(2 to_power i)) > log (2,(((N-bound C) - (S-bound C)) / r)) by A3, POWER:def_3; then 2 to_power i > ((N-bound C) - (S-bound C)) / r by A3, PRE_FF:10; then 2 |^ i > ((N-bound C) - (S-bound C)) / r by POWER:41; then (2 |^ i) * r > (((N-bound C) - (S-bound C)) / r) * r by A1, XREAL_1:68; then (2 |^ i) * r > (N-bound C) - (S-bound C) by A1, XCMPLX_1:87; then ((2 |^ i) * r) / (2 |^ i) > ((N-bound C) - (S-bound C)) / (2 |^ i) by A4, XREAL_1:74; then A8: ((N-bound C) - (S-bound C)) / (2 |^ i) < r by A4, XCMPLX_1:89; ( (abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1 >= 0 + 1 & max (((abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1),((abs [\(log (2,(((E-bound C) - (W-bound C)) / t)))/]) + 1)) >= (abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1 ) by XREAL_1:7, XXREAL_0:25; then max (((abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1),((abs [\(log (2,(((E-bound C) - (W-bound C)) / t)))/]) + 1)) >= 1 by XXREAL_0:2; then (max (((abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1),((abs [\(log (2,(((E-bound C) - (W-bound C)) / t)))/]) + 1))) + 1 >= 1 + 1 by XREAL_1:7; hence 1 < i by XXREAL_0:2; ::_thesis: ( dist (((Gauge (C,i)) * (1,1)),((Gauge (C,i)) * (1,2))) < r & dist (((Gauge (C,i)) * (1,1)),((Gauge (C,i)) * (2,1))) < t ) A9: len (Gauge (C,i)) >= 4 by JORDAN8:10; then A10: 1 <= len (Gauge (C,i)) by XXREAL_0:2; [\(log (2,(((E-bound C) - (W-bound C)) / t)))/] <= abs [\(log (2,(((E-bound C) - (W-bound C)) / t)))/] by ABSVALUE:4; then A11: [\(log (2,(((E-bound C) - (W-bound C)) / t)))/] + 1 <= (abs [\(log (2,(((E-bound C) - (W-bound C)) / t)))/]) + 1 by XREAL_1:6; [\(log (2,(((E-bound C) - (W-bound C)) / t)))/] > (log (2,(((E-bound C) - (W-bound C)) / t))) - 1 by INT_1:def_6; then [\(log (2,(((E-bound C) - (W-bound C)) / t)))/] + 1 > ((log (2,(((E-bound C) - (W-bound C)) / t))) - 1) + 1 by XREAL_1:6; then A12: (abs [\(log (2,(((E-bound C) - (W-bound C)) / t)))/]) + 1 > ((log (2,(((E-bound C) - (W-bound C)) / t))) - 1) + 1 by A11, XXREAL_0:2; (abs [\(log (2,(((E-bound C) - (W-bound C)) / t)))/]) + 1 <= max (((abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1),((abs [\(log (2,(((E-bound C) - (W-bound C)) / t)))/]) + 1)) by XXREAL_0:25; then A13: ((abs [\(log (2,(((E-bound C) - (W-bound C)) / t)))/]) + 1) + 1 <= (max (((abs [\(log (2,(((N-bound C) - (S-bound C)) / r)))/]) + 1),((abs [\(log (2,(((E-bound C) - (W-bound C)) / t)))/]) + 1))) + 1 by XREAL_1:6; (abs [\(log (2,(((E-bound C) - (W-bound C)) / t)))/]) + 1 < ((abs [\(log (2,(((E-bound C) - (W-bound C)) / t)))/]) + 1) + 1 by XREAL_1:29; then i > (abs [\(log (2,(((E-bound C) - (W-bound C)) / t)))/]) + 1 by A13, XXREAL_0:2; then i > log (2,(((E-bound C) - (W-bound C)) / t)) by A12, XXREAL_0:2; then log (2,(2 to_power i)) > log (2,(((E-bound C) - (W-bound C)) / t)) by A3, POWER:def_3; then 2 to_power i > ((E-bound C) - (W-bound C)) / t by A3, PRE_FF:10; then 2 |^ i > ((E-bound C) - (W-bound C)) / t by POWER:41; then (2 |^ i) * t > (((E-bound C) - (W-bound C)) / t) * t by A2, XREAL_1:68; then (2 |^ i) * t > (E-bound C) - (W-bound C) by A2, XCMPLX_1:87; then ((2 |^ i) * t) / (2 |^ i) > ((E-bound C) - (W-bound C)) / (2 |^ i) by A4, XREAL_1:74; then A14: ((E-bound C) - (W-bound C)) / (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_1:36; 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_1:36; [(1 + 1),1] in Indices (Gauge (C,i)) by A15, A10, A17, MATRIX_1:36; hence ( dist (((Gauge (C,i)) * (1,1)),((Gauge (C,i)) * (1,2))) < r & dist (((Gauge (C,i)) * (1,1)),((Gauge (C,i)) * (2,1))) < t ) by A8, A14, A16, A18, Th9, Th10; ::_thesis: verum end; begin theorem Th12: :: GOBRD14:12 for f being non constant standard special_circular_sequence for P being Subset of ((TOP-REAL 2) | ((L~ f) `)) holds ( not P is a_component or P = RightComp f or P = LeftComp f ) proof let f be non constant standard special_circular_sequence; ::_thesis: for P being Subset of ((TOP-REAL 2) | ((L~ f) `)) holds ( not P is a_component or P = RightComp f or P = LeftComp f ) let P be Subset of ((TOP-REAL 2) | ((L~ f) `)); ::_thesis: ( not P is a_component or P = RightComp f or P = LeftComp f ) assume that A1: P is a_component and A2: P <> RightComp f ; ::_thesis: P = LeftComp 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 P = LeftComp f by A1, A5, CONNSP_1:35; ::_thesis: verum end; theorem :: GOBRD14:13 for f being non constant standard special_circular_sequence 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 ) ) & not ( A1 = RightComp f & A2 = LeftComp f ) holds ( A1 = LeftComp f & A2 = RightComp f ) proof let f be non constant standard special_circular_sequence; ::_thesis: 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 ) ) & not ( A1 = RightComp f & A2 = LeftComp f ) holds ( A1 = LeftComp f & A2 = RightComp f ) let A1, A2 be Subset of (TOP-REAL 2); ::_thesis: ( (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 ) ) & not ( A1 = RightComp f & A2 = LeftComp f ) implies ( A1 = LeftComp f & A2 = RightComp f ) ) assume 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 ) ; :: according to XBOOLE_0:def_7 ::_thesis: ( ( A1 = RightComp f & A2 = LeftComp f ) or ( A1 = LeftComp f & A2 = RightComp f ) ) 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 ( A1 = RightComp f & A2 = LeftComp f ) & not ( A1 = LeftComp f & A2 = RightComp f ) ) ; ::_thesis: contradiction hence contradiction by A2, A5, A4; ::_thesis: verum end; theorem Th14: :: GOBRD14:14 for f being non constant standard special_circular_sequence holds LeftComp f misses RightComp f proof let f be non constant standard special_circular_sequence; ::_thesis: LeftComp f misses RightComp f assume (LeftComp f) /\ (RightComp f) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction then consider x being set such that A1: x in (LeftComp f) /\ (RightComp f) by XBOOLE_0:def_1; now__::_thesis:_ex_x_being_set_st_ (_x_in_LeftComp_f_&_x_in_RightComp_f_) take x = x; ::_thesis: ( x in LeftComp f & x in RightComp f ) thus ( x in LeftComp f & x in RightComp f ) by A1, XBOOLE_0:def_4; ::_thesis: verum 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, GOBOARD9:def_2; hence contradiction by A2, GOBOARD9:1, SPRECT_4:6; ::_thesis: verum end; theorem Th15: :: GOBRD14:15 for f being non constant standard special_circular_sequence holds ((L~ f) \/ (RightComp f)) \/ (LeftComp f) = the carrier of (TOP-REAL 2) proof let f be non constant standard special_circular_sequence; ::_thesis: ((L~ f) \/ (RightComp f)) \/ (LeftComp f) = the carrier of (TOP-REAL 2) 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 ((L~ f) \/ (RightComp f)) \/ (LeftComp f) = the carrier of (TOP-REAL 2) by A1, XBOOLE_1:4; ::_thesis: verum end; theorem Th16: :: GOBRD14:16 for f being non constant standard special_circular_sequence for p being Point of (TOP-REAL 2) holds ( p in L~ f iff ( not p in LeftComp f & not p in RightComp f ) ) proof let f be non constant standard special_circular_sequence; ::_thesis: for p being Point of (TOP-REAL 2) holds ( p in L~ f iff ( not p in LeftComp f & not p in RightComp f ) ) let p be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f iff ( not p in LeftComp f & not p in RightComp f ) ) 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 ( p in L~ f iff ( not p in LeftComp f & not p in RightComp f ) ) by A1, XBOOLE_0:def_3; ::_thesis: verum end; theorem Th17: :: GOBRD14:17 for f being non constant standard special_circular_sequence for p being Point of (TOP-REAL 2) holds ( p in LeftComp f iff ( not p in L~ f & not p in RightComp f ) ) proof let f be non constant standard special_circular_sequence; ::_thesis: for p being Point of (TOP-REAL 2) holds ( p in LeftComp f iff ( not p in L~ f & not p in RightComp f ) ) let p be Point of (TOP-REAL 2); ::_thesis: ( p in LeftComp f iff ( not p in L~ f & not p in RightComp f ) ) LeftComp f misses RightComp f by Th14; then A1: ( (L~ f) ` = (LeftComp f) \/ (RightComp f) & (LeftComp f) /\ (RightComp f) = {} ) by GOBRD12:10, XBOOLE_0:def_7; ( p in L~ f iff not p in (L~ f) ` ) by XBOOLE_0:def_5; hence ( p in LeftComp f iff ( not p in L~ f & not p in RightComp f ) ) by A1, XBOOLE_0:def_3, XBOOLE_0:def_4; ::_thesis: verum end; theorem :: GOBRD14:18 for f being non constant standard special_circular_sequence for p being Point of (TOP-REAL 2) holds ( p in RightComp f iff ( not p in L~ f & not p in LeftComp f ) ) by Th16, Th17; theorem Th19: :: GOBRD14:19 for f being non constant standard special_circular_sequence holds L~ f = (Cl (RightComp f)) \ (RightComp f) proof let f be non constant standard special_circular_sequence; ::_thesis: L~ f = (Cl (RightComp f)) \ (RightComp f) thus L~ f c= (Cl (RightComp f)) \ (RightComp f) :: according to XBOOLE_0:def_10 ::_thesis: (Cl (RightComp f)) \ (RightComp f) c= L~ f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L~ f or x in (Cl (RightComp f)) \ (RightComp f) ) assume A1: x in L~ f ; ::_thesis: x in (Cl (RightComp f)) \ (RightComp f) then reconsider p = x as Point of (TOP-REAL 2) ; consider i being Element of NAT 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 & p in O holds 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 Element of 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_1:38; A11: j2 <= width (GoB f) by A7, MATRIX_1:38; A12: 1 <= j1 by A5, MATRIX_1:38; A13: j1 <= width (GoB f) by A5, MATRIX_1:38; A14: i1 <= len (GoB f) by A5, MATRIX_1:38; A15: i2 <= len (GoB f) by A7, MATRIX_1:38; A16: now__::_thesis:_(_(_i1_=_i2_&_j1_+_1_=_j2_&_p_in_Cl_(Int_(right_cell_(f,i)))_)_or_(_i1_+_1_=_i2_&_j1_=_j2_&_p_in_Cl_(Int_(right_cell_(f,i)))_)_or_(_i1_=_i2_+_1_&_j1_=_j2_&_p_in_Cl_(Int_(right_cell_(f,i)))_)_or_(_i1_=_i2_&_j1_=_j2_+_1_&_p_in_Cl_(Int_(right_cell_(f,i)))_)_) 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 A9; caseA17: ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: p in Cl (Int (right_cell (f,i))) set w = i1 -' 1; A18: (i1 -' 1) + 1 = i1 by A10, XREAL_1:235; then right_cell (f,i) = cell ((GoB f),((i1 -' 1) + 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; ::_thesis: verum end; caseA19: ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: p in Cl (Int (right_cell (f,i))) set w = j1 -' 1; ( j1 -' 1 <= (j1 -' 1) + 1 & (j1 -' 1) + 1 <= width (GoB f) ) by A12, A13, NAT_1:11, XREAL_1:235; then A20: j1 -' 1 <= width (GoB f) by XXREAL_0:2; (j1 -' 1) + 1 = j1 by A12, XREAL_1:235; then right_cell (f,i) = cell ((GoB f),i1,(j1 -' 1)) by A2, A5, A6, A7, A8, A19, GOBOARD5:28; hence p in Cl (Int (right_cell (f,i))) by A4, A14, A20, GOBRD11:35; ::_thesis: verum end; caseA21: ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: p in Cl (Int (right_cell (f,i))) set w = j1 -' 1; A22: (j1 -' 1) + 1 = j1 by A12, XREAL_1:235; then right_cell (f,i) = cell ((GoB f),i2,((j1 -' 1) + 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; ::_thesis: verum end; caseA23: ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: p in Cl (Int (right_cell (f,i))) set z = i1 -' 1; ( i1 -' 1 <= (i1 -' 1) + 1 & (i1 -' 1) + 1 <= len (GoB f) ) by A10, A14, NAT_1:11, XREAL_1:235; then A24: i1 -' 1 <= len (GoB f) by XXREAL_0:2; (i1 -' 1) + 1 = i1 by A10, XREAL_1:235; then right_cell (f,i) = cell ((GoB f),(i1 -' 1),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; ::_thesis: verum end; end; end; let O be Subset of (TOP-REAL 2); ::_thesis: ( O is open & p in O implies RightComp f meets O ) assume ( O is open & p in O ) ; ::_thesis: RightComp f meets O then O meets Int (right_cell (f,i)) by A16, PRE_TOPC:def_7; hence RightComp f meets O by A2, GOBOARD9:25, XBOOLE_1:63; ::_thesis: verum end; then A25: p in Cl (RightComp f) by PRE_TOPC:def_7; not x in RightComp f by A1, Th16; hence x in (Cl (RightComp f)) \ (RightComp f) by A25, XBOOLE_0:def_5; ::_thesis: verum end; assume not (Cl (RightComp f)) \ (RightComp f) c= L~ f ; ::_thesis: contradiction then consider q being set such that A26: q in (Cl (RightComp f)) \ (RightComp f) and A27: not q in L~ f by TARSKI:def_3; reconsider q = 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; ::_thesis: verum end; theorem Th20: :: GOBRD14:20 for f being non constant standard special_circular_sequence holds L~ f = (Cl (LeftComp f)) \ (LeftComp f) proof let f be non constant standard special_circular_sequence; ::_thesis: L~ f = (Cl (LeftComp f)) \ (LeftComp f) thus L~ f c= (Cl (LeftComp f)) \ (LeftComp f) :: according to XBOOLE_0:def_10 ::_thesis: (Cl (LeftComp f)) \ (LeftComp f) c= L~ f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L~ f or x in (Cl (LeftComp f)) \ (LeftComp f) ) assume A1: x in L~ f ; ::_thesis: x in (Cl (LeftComp f)) \ (LeftComp f) then reconsider p = x as Point of (TOP-REAL 2) ; consider i being Element of NAT 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 & p in O holds 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 Element of 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_1:38; A11: j2 <= width (GoB f) by A7, MATRIX_1:38; A12: 1 <= j1 by A5, MATRIX_1:38; A13: j1 <= width (GoB f) by A5, MATRIX_1:38; A14: i1 <= len (GoB f) by A5, MATRIX_1:38; A15: i2 <= len (GoB f) by A7, MATRIX_1:38; A16: now__::_thesis:_(_(_i1_=_i2_&_j1_+_1_=_j2_&_p_in_Cl_(Int_(left_cell_(f,i)))_)_or_(_i1_+_1_=_i2_&_j1_=_j2_&_p_in_Cl_(Int_(left_cell_(f,i)))_)_or_(_i1_=_i2_+_1_&_j1_=_j2_&_p_in_Cl_(Int_(left_cell_(f,i)))_)_or_(_i1_=_i2_&_j1_=_j2_+_1_&_p_in_Cl_(Int_(left_cell_(f,i)))_)_) 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 A9; caseA17: ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: p in Cl (Int (left_cell (f,i))) set w = i1 -' 1; ( i1 -' 1 <= (i1 -' 1) + 1 & (i1 -' 1) + 1 <= len (GoB f) ) by A10, A14, NAT_1:11, XREAL_1:235; then A18: i1 -' 1 <= len (GoB f) by XXREAL_0:2; (i1 -' 1) + 1 = i1 by A10, XREAL_1:235; then left_cell (f,i) = cell ((GoB f),(i1 -' 1),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; ::_thesis: verum end; caseA19: ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: p in Cl (Int (left_cell (f,i))) set w = j1 -' 1; (j1 -' 1) + 1 = j1 by A12, XREAL_1:235; then A20: left_cell (f,i) = cell ((GoB f),i1,((j1 -' 1) + 1)) by A2, A5, A6, A7, A8, A19, GOBOARD5:28; (j1 -' 1) + 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; ::_thesis: verum end; caseA21: ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: p in Cl (Int (left_cell (f,i))) set w = j1 -' 1; ( j1 -' 1 <= (j1 -' 1) + 1 & (j1 -' 1) + 1 <= width (GoB f) ) by A12, A13, NAT_1:11, XREAL_1:235; then A22: j1 -' 1 <= width (GoB f) by XXREAL_0:2; (j1 -' 1) + 1 = j1 by A12, XREAL_1:235; then left_cell (f,i) = cell ((GoB f),i2,(j1 -' 1)) by A2, A5, A6, A7, A8, A21, GOBOARD5:29; hence p in Cl (Int (left_cell (f,i))) by A4, A15, A22, GOBRD11:35; ::_thesis: verum end; caseA23: ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: p in Cl (Int (left_cell (f,i))) set z = i1 -' 1; (i1 -' 1) + 1 = i1 by A10, XREAL_1:235; then A24: left_cell (f,i) = cell ((GoB f),((i1 -' 1) + 1),j2) by A2, A5, A6, A7, A8, A23, GOBOARD5:30; (i1 -' 1) + 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; ::_thesis: verum end; end; end; let O be Subset of (TOP-REAL 2); ::_thesis: ( O is open & p in O implies LeftComp f meets O ) assume ( O is open & p in O ) ; ::_thesis: LeftComp f meets O then O meets Int (left_cell (f,i)) by A16, PRE_TOPC:def_7; hence LeftComp f meets O by A2, GOBOARD9:21, XBOOLE_1:63; ::_thesis: verum end; then A25: p in Cl (LeftComp f) by PRE_TOPC:def_7; not x in LeftComp f by A1, Th16; hence x in (Cl (LeftComp f)) \ (LeftComp f) by A25, XBOOLE_0:def_5; ::_thesis: verum end; assume not (Cl (LeftComp f)) \ (LeftComp f) c= L~ f ; ::_thesis: contradiction then consider q being set such that A26: q in (Cl (LeftComp f)) \ (LeftComp f) and A27: not q in L~ f by TARSKI:def_3; reconsider q = 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; ::_thesis: verum end; theorem Th21: :: GOBRD14:21 for f being non constant standard special_circular_sequence holds Cl (RightComp f) = (RightComp f) \/ (L~ f) proof let f be non constant standard special_circular_sequence; ::_thesis: Cl (RightComp f) = (RightComp f) \/ (L~ f) thus Cl (RightComp f) c= (RightComp f) \/ (L~ f) :: according to XBOOLE_0:def_10 ::_thesis: (RightComp f) \/ (L~ f) c= Cl (RightComp f) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl (RightComp f) or x in (RightComp f) \/ (L~ f) ) assume A1: x in Cl (RightComp f) ; ::_thesis: x in (RightComp f) \/ (L~ f) now__::_thesis:_(_not_x_in_RightComp_f_implies_x_in_L~_f_) A2: now__::_thesis:_not_x_in_LeftComp_f assume x in LeftComp f ; ::_thesis: contradiction then LeftComp f meets RightComp f by A1, TOPS_1:12; hence contradiction by Th14; ::_thesis: verum end; assume not x in RightComp f ; ::_thesis: x in L~ f hence x in L~ f by A1, A2, Th16; ::_thesis: verum end; hence x in (RightComp f) \/ (L~ f) by XBOOLE_0:def_3; ::_thesis: verum 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 (RightComp f) \/ (L~ f) c= Cl (RightComp f) by XBOOLE_1:8; ::_thesis: verum end; theorem :: GOBRD14:22 for f being non constant standard special_circular_sequence holds Cl (LeftComp f) = (LeftComp f) \/ (L~ f) proof let f be non constant standard special_circular_sequence; ::_thesis: Cl (LeftComp f) = (LeftComp f) \/ (L~ f) thus Cl (LeftComp f) c= (LeftComp f) \/ (L~ f) :: according to XBOOLE_0:def_10 ::_thesis: (LeftComp f) \/ (L~ f) c= Cl (LeftComp f) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl (LeftComp f) or x in (LeftComp f) \/ (L~ f) ) assume A1: x in Cl (LeftComp f) ; ::_thesis: x in (LeftComp f) \/ (L~ f) now__::_thesis:_(_not_x_in_LeftComp_f_implies_x_in_L~_f_) A2: now__::_thesis:_not_x_in_RightComp_f assume x in RightComp f ; ::_thesis: contradiction then LeftComp f meets RightComp f by A1, TOPS_1:12; hence contradiction by Th14; ::_thesis: verum end; assume not x in LeftComp f ; ::_thesis: x in L~ f hence x in L~ f by A1, A2, Th16; ::_thesis: verum end; hence x in (LeftComp f) \/ (L~ f) by XBOOLE_0:def_3; ::_thesis: verum 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 (LeftComp f) \/ (L~ f) c= Cl (LeftComp f) by XBOOLE_1:8; ::_thesis: verum end; registration let f be non constant standard special_circular_sequence; cluster L~ f -> Jordan ; coherence L~ f is Jordan proof thus (L~ f) ` <> {} ; :: according to SPRECT_1:def_3 ::_thesis: ex b1, b2 being Element of K19( the carrier of (TOP-REAL 2)) st ( (L~ f) ` = b1 \/ b2 & b1 misses b2 & (Cl b1) \ b1 = (Cl b2) \ b2 & b1 is_a_component_of (L~ f) ` & b2 is_a_component_of (L~ f) ` ) take A1 = RightComp f; ::_thesis: ex b1 being Element of K19( the carrier of (TOP-REAL 2)) st ( (L~ f) ` = A1 \/ b1 & A1 misses b1 & (Cl A1) \ A1 = (Cl b1) \ b1 & A1 is_a_component_of (L~ f) ` & b1 is_a_component_of (L~ f) ` ) take A2 = LeftComp f; ::_thesis: ( (L~ f) ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A1 is_a_component_of (L~ f) ` & A2 is_a_component_of (L~ f) ` ) thus (L~ f) ` = A1 \/ A2 by GOBRD12:10; ::_thesis: ( A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A1 is_a_component_of (L~ f) ` & A2 is_a_component_of (L~ f) ` ) L~ f = (Cl A1) \ A1 by Th19; hence ( A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A1 is_a_component_of (L~ f) ` & A2 is_a_component_of (L~ f) ` ) by Th14, Th20, GOBOARD9:def_1, GOBOARD9:def_2; ::_thesis: verum end; end; theorem Th23: :: GOBRD14:23 for p being Point of (TOP-REAL 2) for f being non constant standard clockwise_oriented special_circular_sequence st p in RightComp f holds W-bound (L~ f) < p `1 proof let p be Point of (TOP-REAL 2); ::_thesis: for f being non constant standard clockwise_oriented special_circular_sequence st p in RightComp f holds W-bound (L~ f) < p `1 let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( p in RightComp f implies W-bound (L~ f) < p `1 ) set g = Rotate (f,(N-min (L~ f))); A1: L~ f = L~ (Rotate (f,(N-min (L~ f)))) by REVROT_1:33; reconsider u = p as Point of (Euclid 2) by EUCLID:22; assume p in RightComp f ; ::_thesis: W-bound (L~ f) < p `1 then p in RightComp (Rotate (f,(N-min (L~ f)))) by REVROT_1:37; then u in Int (RightComp (Rotate (f,(N-min (L~ f))))) by TOPS_1:23; then consider r being real number such that A2: r > 0 and A3: Ball (u,r) c= RightComp (Rotate (f,(N-min (L~ f)))) by GOBOARD6:5; reconsider r = r as Real by XREAL_0:def_1; 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 (Rotate (f,(N-min (L~ f)))) misses LeftComp (Rotate (f,(N-min (L~ f)))) by Th14; then A5: not |[((p `1) - (r / 2)),(p `2)]| in LeftComp (Rotate (f,(N-min (L~ f)))) by A3, A4, XBOOLE_0:3; set x = |[((p `1) - (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]|; A6: LSeg ((NW-corner (L~ (Rotate (f,(N-min (L~ f)))))),(NE-corner (L~ (Rotate (f,(N-min (L~ f))))))) c= L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))) by SPRECT_3:14; A7: proj1 . |[((p `1) - (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| = |[((p `1) - (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| `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: (Rotate (f,(N-min (L~ f)))) /. 1 = N-min (L~ (Rotate (f,(N-min (L~ f))))) by A1, FINSEQ_6:92; then |[((p `1) - (r / 2)),(p `2)]| `1 <= E-bound (L~ (Rotate (f,(N-min (L~ f))))) by A5, JORDAN2C:111; then (p `1) - (r / 2) <= E-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52; then A9: |[((p `1) - (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| `1 <= E-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52; |[((p `1) - (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| `2 = N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) by EUCLID:52; then A10: |[((p `1) - (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| `2 = N-bound (L~ (Rotate (f,(N-min (L~ f))))) by SPRECT_1:60; |[((p `1) - (r / 2)),(p `2)]| `1 >= W-bound (L~ (Rotate (f,(N-min (L~ f))))) by A8, A5, JORDAN2C:110; then (p `1) - (r / 2) >= W-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52; then A11: |[((p `1) - (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| `1 >= W-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52; LSeg ((NW-corner (L~ (Rotate (f,(N-min (L~ f)))))),(NE-corner (L~ (Rotate (f,(N-min (L~ f))))))) = { q where q is Point of (TOP-REAL 2) : ( q `1 <= E-bound (L~ (Rotate (f,(N-min (L~ f))))) & q `1 >= W-bound (L~ (Rotate (f,(N-min (L~ f))))) & q `2 = N-bound (L~ (Rotate (f,(N-min (L~ f))))) ) } by SPRECT_1:25; then |[((p `1) - (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| in LSeg ((NW-corner (L~ (Rotate (f,(N-min (L~ f)))))),(NE-corner (L~ (Rotate (f,(N-min (L~ f))))))) by A9, A11, A10; then ( proj1 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) is bounded_below & (p `1) - (r / 2) in proj1 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) ) by A6, A7, FUNCT_2:35; then A12: lower_bound (proj1 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))) <= (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~ (Rotate (f,(N-min (L~ f))))))) = W-bound (L~ (Rotate (f,(N-min (L~ f))))) & W-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) = lower_bound (proj1 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))) ) by SPRECT_1:43, SPRECT_1:58; hence W-bound (L~ f) < p `1 by A1, A12, A13, XXREAL_0:2; ::_thesis: verum end; theorem Th24: :: GOBRD14:24 for p being Point of (TOP-REAL 2) for f being non constant standard clockwise_oriented special_circular_sequence st p in RightComp f holds E-bound (L~ f) > p `1 proof let p be Point of (TOP-REAL 2); ::_thesis: for f being non constant standard clockwise_oriented special_circular_sequence st p in RightComp f holds E-bound (L~ f) > p `1 let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( p in RightComp f implies E-bound (L~ f) > p `1 ) set g = Rotate (f,(N-min (L~ f))); A1: L~ f = L~ (Rotate (f,(N-min (L~ f)))) by REVROT_1:33; reconsider u = p as Point of (Euclid 2) by EUCLID:22; assume p in RightComp f ; ::_thesis: E-bound (L~ f) > p `1 then p in RightComp (Rotate (f,(N-min (L~ f)))) by REVROT_1:37; then u in Int (RightComp (Rotate (f,(N-min (L~ f))))) by TOPS_1:23; then consider r being real number such that A2: r > 0 and A3: Ball (u,r) c= RightComp (Rotate (f,(N-min (L~ f)))) by GOBOARD6:5; reconsider r = r as Real by XREAL_0:def_1; 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 (Rotate (f,(N-min (L~ f)))) misses LeftComp (Rotate (f,(N-min (L~ f)))) by Th14; then A5: not |[((p `1) + (r / 2)),(p `2)]| in LeftComp (Rotate (f,(N-min (L~ f)))) by A3, A4, XBOOLE_0:3; set x = |[((p `1) + (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]|; A6: LSeg ((NW-corner (L~ (Rotate (f,(N-min (L~ f)))))),(NE-corner (L~ (Rotate (f,(N-min (L~ f))))))) c= L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))) by SPRECT_3:14; A7: proj1 . |[((p `1) + (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| = |[((p `1) + (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| `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: (Rotate (f,(N-min (L~ f)))) /. 1 = N-min (L~ (Rotate (f,(N-min (L~ f))))) by A1, FINSEQ_6:92; then |[((p `1) + (r / 2)),(p `2)]| `1 <= E-bound (L~ (Rotate (f,(N-min (L~ f))))) by A5, JORDAN2C:111; then (p `1) + (r / 2) <= E-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52; then A9: |[((p `1) + (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| `1 <= E-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52; |[((p `1) + (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| `2 = N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) by EUCLID:52; then A10: |[((p `1) + (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| `2 = N-bound (L~ (Rotate (f,(N-min (L~ f))))) by SPRECT_1:60; |[((p `1) + (r / 2)),(p `2)]| `1 >= W-bound (L~ (Rotate (f,(N-min (L~ f))))) by A8, A5, JORDAN2C:110; then (p `1) + (r / 2) >= W-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52; then A11: |[((p `1) + (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| `1 >= W-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52; LSeg ((NW-corner (L~ (Rotate (f,(N-min (L~ f)))))),(NE-corner (L~ (Rotate (f,(N-min (L~ f))))))) = { q where q is Point of (TOP-REAL 2) : ( q `1 <= E-bound (L~ (Rotate (f,(N-min (L~ f))))) & q `1 >= W-bound (L~ (Rotate (f,(N-min (L~ f))))) & q `2 = N-bound (L~ (Rotate (f,(N-min (L~ f))))) ) } by SPRECT_1:25; then |[((p `1) + (r / 2)),(N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))))]| in LSeg ((NW-corner (L~ (Rotate (f,(N-min (L~ f)))))),(NE-corner (L~ (Rotate (f,(N-min (L~ f))))))) by A9, A11, A10; then ( proj1 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) is bounded_above & (p `1) + (r / 2) in proj1 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) ) by A6, A7, FUNCT_2:35; then A12: upper_bound (proj1 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))) >= (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~ (Rotate (f,(N-min (L~ f))))))) = E-bound (L~ (Rotate (f,(N-min (L~ f))))) & E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) = upper_bound (proj1 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))) ) by SPRECT_1:46, SPRECT_1:61; hence E-bound (L~ f) > p `1 by A1, A12, A13, XXREAL_0:2; ::_thesis: verum end; theorem Th25: :: GOBRD14:25 for p being Point of (TOP-REAL 2) for f being non constant standard clockwise_oriented special_circular_sequence st p in RightComp f holds N-bound (L~ f) > p `2 proof let p be Point of (TOP-REAL 2); ::_thesis: for f being non constant standard clockwise_oriented special_circular_sequence st p in RightComp f holds N-bound (L~ f) > p `2 let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( p in RightComp f implies N-bound (L~ f) > p `2 ) set g = Rotate (f,(N-min (L~ f))); A1: L~ f = L~ (Rotate (f,(N-min (L~ f)))) by REVROT_1:33; reconsider u = p as Point of (Euclid 2) by EUCLID:22; assume p in RightComp f ; ::_thesis: N-bound (L~ f) > p `2 then p in RightComp (Rotate (f,(N-min (L~ f)))) by REVROT_1:37; then u in Int (RightComp (Rotate (f,(N-min (L~ f))))) by TOPS_1:23; then consider r being real number such that A2: r > 0 and A3: Ball (u,r) c= RightComp (Rotate (f,(N-min (L~ f)))) by GOBOARD6:5; reconsider r = r as Real by XREAL_0:def_1; 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 (Rotate (f,(N-min (L~ f)))) misses LeftComp (Rotate (f,(N-min (L~ f)))) by Th14; then A5: not |[(p `1),((p `2) + (r / 2))]| in LeftComp (Rotate (f,(N-min (L~ f)))) by A3, A4, XBOOLE_0:3; set x = |[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) + (r / 2))]|; A6: LSeg ((SE-corner (L~ (Rotate (f,(N-min (L~ f)))))),(NE-corner (L~ (Rotate (f,(N-min (L~ f))))))) c= L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))) by TOPREAL6:35; A7: proj2 . |[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) + (r / 2))]| = |[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) + (r / 2))]| `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: (Rotate (f,(N-min (L~ f)))) /. 1 = N-min (L~ (Rotate (f,(N-min (L~ f))))) by A1, FINSEQ_6:92; then |[(p `1),((p `2) + (r / 2))]| `2 <= N-bound (L~ (Rotate (f,(N-min (L~ f))))) by A5, JORDAN2C:113; then (p `2) + (r / 2) <= N-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52; then A9: |[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) + (r / 2))]| `2 <= N-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52; |[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) + (r / 2))]| `1 = E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) by EUCLID:52; then A10: |[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) + (r / 2))]| `1 = E-bound (L~ (Rotate (f,(N-min (L~ f))))) by SPRECT_1:61; |[(p `1),((p `2) + (r / 2))]| `2 >= S-bound (L~ (Rotate (f,(N-min (L~ f))))) by A8, A5, JORDAN2C:112; then (p `2) + (r / 2) >= S-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52; then A11: |[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) + (r / 2))]| `2 >= S-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52; LSeg ((SE-corner (L~ (Rotate (f,(N-min (L~ f)))))),(NE-corner (L~ (Rotate (f,(N-min (L~ f))))))) = { q where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ (Rotate (f,(N-min (L~ f))))) & q `2 <= N-bound (L~ (Rotate (f,(N-min (L~ f))))) & q `2 >= S-bound (L~ (Rotate (f,(N-min (L~ f))))) ) } by SPRECT_1:23; then |[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) + (r / 2))]| in LSeg ((SE-corner (L~ (Rotate (f,(N-min (L~ f)))))),(NE-corner (L~ (Rotate (f,(N-min (L~ f))))))) by A9, A11, A10; then ( proj2 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) is bounded_above & (p `2) + (r / 2) in proj2 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) ) by A6, A7, FUNCT_2:35; then A12: upper_bound (proj2 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))) >= (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~ (Rotate (f,(N-min (L~ f))))))) = N-bound (L~ (Rotate (f,(N-min (L~ f))))) & N-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) = upper_bound (proj2 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))) ) by SPRECT_1:45, SPRECT_1:60; hence N-bound (L~ f) > p `2 by A1, A12, A13, XXREAL_0:2; ::_thesis: verum end; theorem Th26: :: GOBRD14:26 for p being Point of (TOP-REAL 2) for f being non constant standard clockwise_oriented special_circular_sequence st p in RightComp f holds S-bound (L~ f) < p `2 proof let p be Point of (TOP-REAL 2); ::_thesis: for f being non constant standard clockwise_oriented special_circular_sequence st p in RightComp f holds S-bound (L~ f) < p `2 let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( p in RightComp f implies S-bound (L~ f) < p `2 ) set g = Rotate (f,(N-min (L~ f))); A1: L~ f = L~ (Rotate (f,(N-min (L~ f)))) by REVROT_1:33; reconsider u = p as Point of (Euclid 2) by EUCLID:22; assume p in RightComp f ; ::_thesis: S-bound (L~ f) < p `2 then p in RightComp (Rotate (f,(N-min (L~ f)))) by REVROT_1:37; then u in Int (RightComp (Rotate (f,(N-min (L~ f))))) by TOPS_1:23; then consider r being real number such that A2: r > 0 and A3: Ball (u,r) c= RightComp (Rotate (f,(N-min (L~ f)))) by GOBOARD6:5; reconsider r = r as Real by XREAL_0:def_1; 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 (Rotate (f,(N-min (L~ f)))) misses LeftComp (Rotate (f,(N-min (L~ f)))) by Th14; then A5: not |[(p `1),((p `2) - (r / 2))]| in LeftComp (Rotate (f,(N-min (L~ f)))) by A3, A4, XBOOLE_0:3; set x = |[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) - (r / 2))]|; A6: LSeg ((SE-corner (L~ (Rotate (f,(N-min (L~ f)))))),(NE-corner (L~ (Rotate (f,(N-min (L~ f))))))) c= L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))) by TOPREAL6:35; A7: proj2 . |[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) - (r / 2))]| = |[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) - (r / 2))]| `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: (Rotate (f,(N-min (L~ f)))) /. 1 = N-min (L~ (Rotate (f,(N-min (L~ f))))) by A1, FINSEQ_6:92; then |[(p `1),((p `2) - (r / 2))]| `2 <= N-bound (L~ (Rotate (f,(N-min (L~ f))))) by A5, JORDAN2C:113; then (p `2) - (r / 2) <= N-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52; then A9: |[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) - (r / 2))]| `2 <= N-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52; |[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) - (r / 2))]| `1 = E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) by EUCLID:52; then A10: |[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) - (r / 2))]| `1 = E-bound (L~ (Rotate (f,(N-min (L~ f))))) by SPRECT_1:61; |[(p `1),((p `2) - (r / 2))]| `2 >= S-bound (L~ (Rotate (f,(N-min (L~ f))))) by A8, A5, JORDAN2C:112; then (p `2) - (r / 2) >= S-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52; then A11: |[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) - (r / 2))]| `2 >= S-bound (L~ (Rotate (f,(N-min (L~ f))))) by EUCLID:52; LSeg ((SE-corner (L~ (Rotate (f,(N-min (L~ f)))))),(NE-corner (L~ (Rotate (f,(N-min (L~ f))))))) = { q where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ (Rotate (f,(N-min (L~ f))))) & q `2 <= N-bound (L~ (Rotate (f,(N-min (L~ f))))) & q `2 >= S-bound (L~ (Rotate (f,(N-min (L~ f))))) ) } by SPRECT_1:23; then |[(E-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))),((p `2) - (r / 2))]| in LSeg ((SE-corner (L~ (Rotate (f,(N-min (L~ f)))))),(NE-corner (L~ (Rotate (f,(N-min (L~ f))))))) by A9, A11, A10; then ( proj2 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) is bounded_below & (p `2) - (r / 2) in proj2 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) ) by A6, A7, FUNCT_2:35; then A12: lower_bound (proj2 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))) <= (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~ (Rotate (f,(N-min (L~ f))))))) = S-bound (L~ (Rotate (f,(N-min (L~ f))))) & S-bound (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f))))))) = lower_bound (proj2 .: (L~ (SpStSeq (L~ (Rotate (f,(N-min (L~ f)))))))) ) by SPRECT_1:44, SPRECT_1:59; hence S-bound (L~ f) < p `2 by A1, A12, A13, XXREAL_0:2; ::_thesis: verum end; theorem Th27: :: GOBRD14:27 for p, q being Point of (TOP-REAL 2) for f being non constant standard clockwise_oriented special_circular_sequence st p in RightComp f & q in LeftComp f holds LSeg (p,q) meets L~ f proof let p, q be Point of (TOP-REAL 2); ::_thesis: for f being non constant standard clockwise_oriented special_circular_sequence st p in RightComp f & q in LeftComp f holds LSeg (p,q) meets L~ f let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( p in RightComp f & q in LeftComp f implies LSeg (p,q) meets L~ f ) assume that A1: p in RightComp f and A2: q in LeftComp f ; ::_thesis: LSeg (p,q) meets L~ f assume LSeg (p,q) misses L~ f ; ::_thesis: contradiction 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; ::_thesis: verum end; theorem Th28: :: GOBRD14:28 for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds 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 let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: 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))).])) 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 ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) = {1,2} by FUNCT_4:62; A2: Cl (RightComp (SpStSeq C)) = (RightComp (SpStSeq C)) \/ (L~ (SpStSeq C)) by Th21; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: product ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) c= Cl (RightComp (SpStSeq C)) let a be set ; ::_thesis: ( a in Cl (RightComp (SpStSeq C)) implies a in product ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) ) assume A3: a in Cl (RightComp (SpStSeq C)) ; ::_thesis: a in product ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) then reconsider b = a as Point of (TOP-REAL 2) ; reconsider h = a as FinSequence by A3; A4: for x being set st x in {1,2} holds h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x proof let x be set ; ::_thesis: ( x in {1,2} implies h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x ) assume A5: x in {1,2} ; ::_thesis: h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x percases ( x = 1 or x = 2 ) by A5, TARSKI:def_2; supposeA6: x = 1 ; ::_thesis: h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x then A7: ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x = [.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).] by FUNCT_4:63; now__::_thesis:_(_(_a_in_RightComp_(SpStSeq_C)_&_h_._x_in_((1,2)_-->_([.(W-bound_(L~_(SpStSeq_C))),(E-bound_(L~_(SpStSeq_C))).],[.(S-bound_(L~_(SpStSeq_C))),(N-bound_(L~_(SpStSeq_C))).]))_._x_)_or_(_a_in_L~_(SpStSeq_C)_&_h_._x_in_((1,2)_-->_([.(W-bound_(L~_(SpStSeq_C))),(E-bound_(L~_(SpStSeq_C))).],[.(S-bound_(L~_(SpStSeq_C))),(N-bound_(L~_(SpStSeq_C))).]))_._x_)_) percases ( a in RightComp (SpStSeq C) or a in L~ (SpStSeq C) ) by A2, A3, XBOOLE_0:def_3; case a in RightComp (SpStSeq C) ; ::_thesis: h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x then ( W-bound (L~ (SpStSeq C)) < b `1 & E-bound (L~ (SpStSeq C)) > b `1 ) by Th23, Th24; hence h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x by A6, A7, XXREAL_1:1; ::_thesis: verum end; case a in L~ (SpStSeq C) ; ::_thesis: h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x then ( W-bound (L~ (SpStSeq C)) <= b `1 & b `1 <= E-bound (L~ (SpStSeq C)) ) by PSCOMP_1:24; hence h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x by A6, A7, XXREAL_1:1; ::_thesis: verum end; end; end; hence h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x ; ::_thesis: verum end; supposeA8: x = 2 ; ::_thesis: h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x then A9: ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x = [.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).] by FUNCT_4:63; now__::_thesis:_(_(_a_in_RightComp_(SpStSeq_C)_&_h_._x_in_((1,2)_-->_([.(W-bound_(L~_(SpStSeq_C))),(E-bound_(L~_(SpStSeq_C))).],[.(S-bound_(L~_(SpStSeq_C))),(N-bound_(L~_(SpStSeq_C))).]))_._x_)_or_(_a_in_L~_(SpStSeq_C)_&_h_._x_in_((1,2)_-->_([.(W-bound_(L~_(SpStSeq_C))),(E-bound_(L~_(SpStSeq_C))).],[.(S-bound_(L~_(SpStSeq_C))),(N-bound_(L~_(SpStSeq_C))).]))_._x_)_) percases ( a in RightComp (SpStSeq C) or a in L~ (SpStSeq C) ) by A2, A3, XBOOLE_0:def_3; case a in RightComp (SpStSeq C) ; ::_thesis: h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x then ( S-bound (L~ (SpStSeq C)) < b `2 & N-bound (L~ (SpStSeq C)) > b `2 ) by Th25, Th26; hence h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x by A8, A9, XXREAL_1:1; ::_thesis: verum end; case a in L~ (SpStSeq C) ; ::_thesis: h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x then ( S-bound (L~ (SpStSeq C)) <= b `2 & b `2 <= N-bound (L~ (SpStSeq C)) ) by PSCOMP_1:24; hence h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x by A8, A9, XXREAL_1:1; ::_thesis: verum end; end; end; hence h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x ; ::_thesis: verum end; end; end; a is Tuple of 2, REAL by A3, Lm1, FINSEQ_2:131; then ex r, s being Real st a = <*r,s*> by FINSEQ_2:100; then dom h = {1,2} by FINSEQ_1:2, FINSEQ_1:89; hence a in product ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) by A1, A4, CARD_3:9; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in product ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) or a in Cl (RightComp (SpStSeq C)) ) assume a in product ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) ; ::_thesis: a in Cl (RightComp (SpStSeq C)) then consider h being Function such that A10: a = h and A11: dom h = dom ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) and A12: for x being set st x in dom ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) holds h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . 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 ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) by A1, TARSKI:def_2; then h . 2 in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . 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 ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) by A1, TARSKI:def_2; then h . 1 in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . 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 where q is Point of (TOP-REAL 2) : ( not W-bound (L~ (SpStSeq C)) <= q `1 or not q `1 <= E-bound (L~ (SpStSeq C)) or not S-bound (L~ (SpStSeq C)) <= q `2 or not q `2 <= N-bound (L~ (SpStSeq C)) ) } by SPRECT_3:37; A20: for k being set st k in dom h holds h . k = <*r,s*> . k proof let k be set ; ::_thesis: ( k in dom h implies h . k = <*r,s*> . k ) assume k in dom h ; ::_thesis: h . k = <*r,s*> . k then ( k = 1 or k = 2 ) by A11, TARSKI:def_2; hence h . k = <*r,s*> . k by A17, A14, FINSEQ_1:44; ::_thesis: verum end; dom <*r,s*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89; then A21: a = |[r,s]| by A10, A11, A20, FUNCT_1:2, FUNCT_4:62; assume not a in Cl (RightComp (SpStSeq C)) ; ::_thesis: contradiction 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 being Point of (TOP-REAL 2) st ( q = a & ( not W-bound (L~ (SpStSeq C)) <= q `1 or not q `1 <= E-bound (L~ (SpStSeq C)) or not S-bound (L~ (SpStSeq C)) <= q `2 or not q `2 <= N-bound (L~ (SpStSeq C)) ) ) by A19; hence contradiction by A18, A15, A21, EUCLID:52; ::_thesis: verum end; theorem Th29: :: GOBRD14:29 for f being non constant standard clockwise_oriented special_circular_sequence holds proj1 .: (Cl (RightComp f)) = proj1 .: (L~ f) proof let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: proj1 .: (Cl (RightComp f)) = proj1 .: (L~ f) set g = Rotate (f,(N-min (L~ f))); A1: L~ f = L~ (Rotate (f,(N-min (L~ f)))) by REVROT_1:33; N-min (L~ f) in rng f by SPRECT_2:39; then A2: (Rotate (f,(N-min (L~ f)))) /. 1 = N-min (L~ (Rotate (f,(N-min (L~ f))))) by A1, FINSEQ_6:92; thus proj1 .: (Cl (RightComp f)) c= proj1 .: (L~ f) :: according to XBOOLE_0:def_10 ::_thesis: proj1 .: (L~ f) c= proj1 .: (Cl (RightComp f)) proof A3: Cl (RightComp f) = (RightComp f) \/ (L~ f) by Th21; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in proj1 .: (Cl (RightComp f)) or a in proj1 .: (L~ f) ) assume a in proj1 .: (Cl (RightComp f)) ; ::_thesis: a in proj1 .: (L~ f) then consider x being set 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; percases ( x in RightComp f or x in L~ f ) by A5, A3, XBOOLE_0:def_3; supposeA7: x in RightComp f ; ::_thesis: a in proj1 .: (L~ f) reconsider x = x as Point of (TOP-REAL 2) by A4; set b = |[(x `1),((N-bound (L~ f)) + 1)]|; ( |[(x `1),((N-bound (L~ f)) + 1)]| `2 = (N-bound (L~ f)) + 1 & (N-bound (L~ f)) + 1 > (N-bound (L~ f)) + 0 ) by EUCLID:52, XREAL_1:6; then |[(x `1),((N-bound (L~ f)) + 1)]| in LeftComp (Rotate (f,(N-min (L~ f)))) by A1, A2, JORDAN2C:113; then |[(x `1),((N-bound (L~ f)) + 1)]| in LeftComp f by REVROT_1:36; then LSeg (x,|[(x `1),((N-bound (L~ f)) + 1)]|) meets L~ f by A7, Th27; then consider c being set such that A8: c in LSeg (x,|[(x `1),((N-bound (L~ f)) + 1)]|) and A9: c in L~ f by XBOOLE_0:3; reconsider c = c as Point of (TOP-REAL 2) by A8; A10: |[(x `1),((N-bound (L~ f)) + 1)]| `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 a in proj1 .: (L~ f) by A9, FUNCT_2:35; ::_thesis: verum end; suppose x in L~ f ; ::_thesis: a in proj1 .: (L~ f) hence a in proj1 .: (L~ f) by A6, FUNCT_2:35; ::_thesis: verum end; end; end; L~ f = (Cl (RightComp f)) \ (RightComp f) by Th19; hence proj1 .: (L~ f) c= proj1 .: (Cl (RightComp f)) by RELAT_1:123, XBOOLE_1:36; ::_thesis: verum end; theorem Th30: :: GOBRD14:30 for f being non constant standard clockwise_oriented special_circular_sequence holds proj2 .: (Cl (RightComp f)) = proj2 .: (L~ f) proof let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: proj2 .: (Cl (RightComp f)) = proj2 .: (L~ f) set g = Rotate (f,(N-min (L~ f))); A1: L~ f = L~ (Rotate (f,(N-min (L~ f)))) by REVROT_1:33; N-min (L~ f) in rng f by SPRECT_2:39; then A2: (Rotate (f,(N-min (L~ f)))) /. 1 = N-min (L~ (Rotate (f,(N-min (L~ f))))) by A1, FINSEQ_6:92; thus proj2 .: (Cl (RightComp f)) c= proj2 .: (L~ f) :: according to XBOOLE_0:def_10 ::_thesis: proj2 .: (L~ f) c= proj2 .: (Cl (RightComp f)) proof A3: Cl (RightComp f) = (RightComp f) \/ (L~ f) by Th21; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in proj2 .: (Cl (RightComp f)) or a in proj2 .: (L~ f) ) assume a in proj2 .: (Cl (RightComp f)) ; ::_thesis: a in proj2 .: (L~ f) then consider x being set 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; percases ( x in RightComp f or x in L~ f ) by A5, A3, XBOOLE_0:def_3; supposeA7: x in RightComp f ; ::_thesis: a in proj2 .: (L~ f) reconsider x = x as Point of (TOP-REAL 2) by A4; set b = |[((E-bound (L~ f)) + 1),(x `2)]|; ( |[((E-bound (L~ f)) + 1),(x `2)]| `1 = (E-bound (L~ f)) + 1 & (E-bound (L~ f)) + 1 > (E-bound (L~ f)) + 0 ) by EUCLID:52, XREAL_1:6; then |[((E-bound (L~ f)) + 1),(x `2)]| in LeftComp (Rotate (f,(N-min (L~ f)))) by A1, A2, JORDAN2C:111; then |[((E-bound (L~ f)) + 1),(x `2)]| in LeftComp f by REVROT_1:36; then LSeg (x,|[((E-bound (L~ f)) + 1),(x `2)]|) meets L~ f by A7, Th27; then consider c being set such that A8: c in LSeg (x,|[((E-bound (L~ f)) + 1),(x `2)]|) and A9: c in L~ f by XBOOLE_0:3; reconsider c = c as Point of (TOP-REAL 2) by A8; A10: |[((E-bound (L~ f)) + 1),(x `2)]| `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 a in proj2 .: (L~ f) by A9, FUNCT_2:35; ::_thesis: verum end; suppose x in L~ f ; ::_thesis: a in proj2 .: (L~ f) hence a in proj2 .: (L~ f) by A6, FUNCT_2:35; ::_thesis: verum end; end; end; L~ f = (Cl (RightComp f)) \ (RightComp f) by Th19; hence proj2 .: (L~ f) c= proj2 .: (Cl (RightComp f)) by RELAT_1:123, XBOOLE_1:36; ::_thesis: verum end; theorem Th31: :: GOBRD14:31 for g being non constant standard clockwise_oriented special_circular_sequence holds RightComp g c= RightComp (SpStSeq (L~ g)) proof let g be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: RightComp g c= RightComp (SpStSeq (L~ g)) let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in RightComp g or a in RightComp (SpStSeq (L~ g)) ) assume A1: a in RightComp g ; ::_thesis: a in RightComp (SpStSeq (L~ 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 where q is Point of (TOP-REAL 2) : ( 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 a in RightComp (SpStSeq (L~ g)) by A2, A4, A3, A5; ::_thesis: verum end; theorem Th32: :: GOBRD14:32 for g being non constant standard clockwise_oriented special_circular_sequence holds Cl (RightComp g) is compact proof let g be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: Cl (RightComp g) is compact 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 Cl (RightComp g) is compact by A1, COMPTS_1:9, PRE_TOPC:19; ::_thesis: verum end; theorem Th33: :: GOBRD14:33 for g being non constant standard clockwise_oriented special_circular_sequence holds not LeftComp g is bounded proof let g be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: not LeftComp g is bounded 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 not LeftComp g is bounded by A1, TOPREAL6:66; ::_thesis: verum end; theorem Th34: :: GOBRD14:34 for g being non constant standard clockwise_oriented special_circular_sequence holds LeftComp g is_outside_component_of L~ g proof let g be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: LeftComp g is_outside_component_of L~ g thus LeftComp g is_a_component_of (L~ g) ` by GOBOARD9:def_1; :: according to JORDAN2C:def_3 ::_thesis: not LeftComp g is bounded thus not LeftComp g is bounded by Th33; ::_thesis: verum end; theorem :: GOBRD14:35 for g being non constant standard clockwise_oriented special_circular_sequence holds RightComp g is_inside_component_of L~ g proof let g be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: RightComp g is_inside_component_of L~ g thus RightComp g is_a_component_of (L~ g) ` by GOBOARD9:def_2; :: according to JORDAN2C:def_2 ::_thesis: RightComp g is bounded Cl (RightComp g) is compact by Th32; hence RightComp g is bounded by PRE_TOPC:18, RLTOPSP1:42; ::_thesis: verum end; theorem Th36: :: GOBRD14:36 for g being non constant standard clockwise_oriented special_circular_sequence holds UBD (L~ g) = LeftComp g proof let g be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: UBD (L~ g) = LeftComp g ( UBD (L~ g) is_outside_component_of L~ g & LeftComp g is_outside_component_of L~ g ) by Th34, JORDAN2C:68; hence UBD (L~ g) = LeftComp g by JORDAN2C:119; ::_thesis: verum end; theorem Th37: :: GOBRD14:37 for g being non constant standard clockwise_oriented special_circular_sequence holds BDD (L~ g) = RightComp g proof let g be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: BDD (L~ g) = RightComp g 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 BDD (L~ g) = RightComp g by A2, A1, XBOOLE_1:71; ::_thesis: verum end; theorem :: GOBRD14:38 for g being non constant standard clockwise_oriented special_circular_sequence for P being Subset of (TOP-REAL 2) st P is_outside_component_of L~ g holds P = LeftComp g proof let g be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for P being Subset of (TOP-REAL 2) st P is_outside_component_of L~ g holds P = LeftComp g let P be Subset of (TOP-REAL 2); ::_thesis: ( P is_outside_component_of L~ g implies P = LeftComp g ) assume A1: P is_outside_component_of L~ g ; ::_thesis: P = LeftComp g UBD (L~ g) is_outside_component_of L~ g by JORDAN2C:68; then P = UBD (L~ g) by A1, JORDAN2C:119; hence P = LeftComp g by Th36; ::_thesis: verum end; theorem Th39: :: GOBRD14:39 for g being non constant standard clockwise_oriented special_circular_sequence for P being Subset of (TOP-REAL 2) st P is_inside_component_of L~ g holds P meets RightComp g proof let g be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for P being Subset of (TOP-REAL 2) st P is_inside_component_of L~ g holds P meets RightComp g let P be Subset of (TOP-REAL 2); ::_thesis: ( P is_inside_component_of L~ g implies P meets RightComp g ) assume P is_inside_component_of L~ g ; ::_thesis: P meets RightComp g then A1: ( P c= BDD (L~ g) & P is_a_component_of (L~ g) ` ) by JORDAN2C:22, JORDAN2C:def_2; BDD (L~ g) = RightComp g by Th37; hence P meets RightComp g by A1, SPRECT_1:4, XBOOLE_1:67; ::_thesis: verum end; theorem :: GOBRD14:40 for g being non constant standard clockwise_oriented special_circular_sequence for P being Subset of (TOP-REAL 2) st P is_inside_component_of L~ g holds P = BDD (L~ g) proof let g be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for P being Subset of (TOP-REAL 2) st P is_inside_component_of L~ g holds P = BDD (L~ g) let P be Subset of (TOP-REAL 2); ::_thesis: ( P is_inside_component_of L~ g implies P = BDD (L~ g) ) 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) ` by JORDAN2C:def_2; assume A3: P is_inside_component_of L~ g ; ::_thesis: P = BDD (L~ g) then P is_a_component_of (L~ g) ` by JORDAN2C:def_2; hence P = BDD (L~ g) by A3, A1, A2, Th39, GOBOARD9:1; ::_thesis: verum end; theorem :: GOBRD14:41 for g being non constant standard clockwise_oriented special_circular_sequence holds W-bound (L~ g) = W-bound (RightComp g) proof let g be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: W-bound (L~ g) = W-bound (RightComp g) 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 = (Cl (RightComp g)) \ (RightComp g) by Th19; Cl (RightComp g) is compact by Th32; then A3: RightComp g is bounded by PRE_TOPC:18, RLTOPSP1:42; reconsider A = (Cl (RightComp g)) \ (RightComp g) 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 W-bound (L~ g) = W-bound (RightComp g) by A2, A3, A1, TOPREAL6:85; ::_thesis: verum end; theorem :: GOBRD14:42 for g being non constant standard clockwise_oriented special_circular_sequence holds E-bound (L~ g) = E-bound (RightComp g) proof let g be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: E-bound (L~ g) = E-bound (RightComp g) 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 = (Cl (RightComp g)) \ (RightComp g) by Th19; Cl (RightComp g) is compact by Th32; then A3: RightComp g is bounded by PRE_TOPC:18, RLTOPSP1:42; reconsider A = (Cl (RightComp g)) \ (RightComp g) 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 E-bound (L~ g) = E-bound (RightComp g) by A2, A3, A1, TOPREAL6:86; ::_thesis: verum end; theorem :: GOBRD14:43 for g being non constant standard clockwise_oriented special_circular_sequence holds N-bound (L~ g) = N-bound (RightComp g) proof let g be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: N-bound (L~ g) = N-bound (RightComp g) 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 = (Cl (RightComp g)) \ (RightComp g) by Th19; Cl (RightComp g) is compact by Th32; then A3: RightComp g is bounded by PRE_TOPC:18, RLTOPSP1:42; reconsider A = (Cl (RightComp g)) \ (RightComp g) 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 N-bound (L~ g) = N-bound (RightComp g) by A2, A3, A1, TOPREAL6:87; ::_thesis: verum end; theorem :: GOBRD14:44 for g being non constant standard clockwise_oriented special_circular_sequence holds S-bound (L~ g) = S-bound (RightComp g) proof let g be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: S-bound (L~ g) = S-bound (RightComp g) 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 = (Cl (RightComp g)) \ (RightComp g) by Th19; Cl (RightComp g) is compact by Th32; then A3: RightComp g is bounded by PRE_TOPC:18, RLTOPSP1:42; reconsider A = (Cl (RightComp g)) \ (RightComp g) 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 S-bound (L~ g) = S-bound (RightComp g) by A2, A3, A1, TOPREAL6:88; ::_thesis: verum end;