:: SPRECT_3 semantic presentation begin theorem :: SPRECT_3:1 for D being non empty set for f being non empty FinSequence of D for g being FinSequence of D holds (g ^ f) /. (len (g ^ f)) = f /. (len f) proof let D be non empty set ; ::_thesis: for f being non empty FinSequence of D for g being FinSequence of D holds (g ^ f) /. (len (g ^ f)) = f /. (len f) let f be non empty FinSequence of D; ::_thesis: for g being FinSequence of D holds (g ^ f) /. (len (g ^ f)) = f /. (len f) let g be FinSequence of D; ::_thesis: (g ^ f) /. (len (g ^ f)) = f /. (len f) A1: len f >= 1 by NAT_1:14; len (g ^ f) = (len g) + (len f) by FINSEQ_1:22; hence (g ^ f) /. (len (g ^ f)) = f /. (len f) by A1, SEQ_4:136; ::_thesis: verum end; theorem Th2: :: SPRECT_3:2 for a, b, c, d being set holds Indices ((a,b) ][ (c,d)) = {[1,1],[1,2],[2,1],[2,2]} proof let a, b, c, d be set ; ::_thesis: Indices ((a,b) ][ (c,d)) = {[1,1],[1,2],[2,1],[2,2]} thus Indices ((a,b) ][ (c,d)) = [:(Seg 2),(Seg 2):] by MATRIX_2:3 .= [:{1},(Seg 2):] \/ [:{2},(Seg 2):] by FINSEQ_1:2, ZFMISC_1:109 .= [:{1},(Seg 2):] \/ {[2,1],[2,2]} by FINSEQ_1:2, ZFMISC_1:30 .= {[1,1],[1,2]} \/ {[2,1],[2,2]} by FINSEQ_1:2, ZFMISC_1:30 .= {[1,1],[1,2],[2,1],[2,2]} by ENUMSET1:5 ; ::_thesis: verum end; begin theorem Th3: :: SPRECT_3:3 for n being Element of NAT for p, q being Point of (TOP-REAL n) for r being Real st 0 < r & p = ((1 - r) * p) + (r * q) holds p = q proof let n be Element of NAT ; ::_thesis: for p, q being Point of (TOP-REAL n) for r being Real st 0 < r & p = ((1 - r) * p) + (r * q) holds p = q let p, q be Point of (TOP-REAL n); ::_thesis: for r being Real st 0 < r & p = ((1 - r) * p) + (r * q) holds p = q let r be Real; ::_thesis: ( 0 < r & p = ((1 - r) * p) + (r * q) implies p = q ) assume that A1: 0 < r and A2: p = ((1 - r) * p) + (r * q) ; ::_thesis: p = q A3: ((1 - r) * p) + (r * p) = ((1 - r) + r) * p by EUCLID:33 .= p by EUCLID:29 ; r * p = (r * p) + (0. (TOP-REAL n)) by EUCLID:27 .= (r * p) + (((1 - r) * p) + (- ((1 - r) * p))) by EUCLID:36 .= ((r * q) + ((1 - r) * p)) + (- ((1 - r) * p)) by A2, A3, EUCLID:26 .= (r * q) + (((1 - r) * p) + (- ((1 - r) * p))) by EUCLID:26 .= (r * q) + (0. (TOP-REAL n)) by EUCLID:36 .= r * q by EUCLID:27 ; hence p = q by A1, EUCLID:34; ::_thesis: verum end; theorem Th4: :: SPRECT_3:4 for n being Element of NAT for p, q being Point of (TOP-REAL n) for r being Real st r < 1 & p = ((1 - r) * q) + (r * p) holds p = q proof let n be Element of NAT ; ::_thesis: for p, q being Point of (TOP-REAL n) for r being Real st r < 1 & p = ((1 - r) * q) + (r * p) holds p = q let p, q be Point of (TOP-REAL n); ::_thesis: for r being Real st r < 1 & p = ((1 - r) * q) + (r * p) holds p = q let r be Real; ::_thesis: ( r < 1 & p = ((1 - r) * q) + (r * p) implies p = q ) assume that A1: r < 1 and A2: p = ((1 - r) * q) + (r * p) ; ::_thesis: p = q set s = 1 - r; r + 0 < 1 by A1; then A3: 0 < 1 - r by XREAL_1:20; p = ((1 - (1 - r)) * p) + ((1 - r) * q) by A2; hence p = q by A3, Th3; ::_thesis: verum end; theorem :: SPRECT_3:5 for n being Element of NAT for p, q being Point of (TOP-REAL n) st p = (1 / 2) * (p + q) holds p = q proof let n be Element of NAT ; ::_thesis: for p, q being Point of (TOP-REAL n) st p = (1 / 2) * (p + q) holds p = q let p, q be Point of (TOP-REAL n); ::_thesis: ( p = (1 / 2) * (p + q) implies p = q ) assume p = (1 / 2) * (p + q) ; ::_thesis: p = q then p = ((1 - (1 / 2)) * p) + ((1 / 2) * q) by EUCLID:32; hence p = q by Th3; ::_thesis: verum end; theorem Th6: :: SPRECT_3:6 for n being Element of NAT for p, q, r being Point of (TOP-REAL n) st q in LSeg (p,r) & r in LSeg (p,q) holds q = r proof let n be Element of NAT ; ::_thesis: for p, q, r being Point of (TOP-REAL n) st q in LSeg (p,r) & r in LSeg (p,q) holds q = r let p, q, r be Point of (TOP-REAL n); ::_thesis: ( q in LSeg (p,r) & r in LSeg (p,q) implies q = r ) assume q in LSeg (p,r) ; ::_thesis: ( not r in LSeg (p,q) or q = r ) then consider r1 being Real such that A1: q = ((1 - r1) * p) + (r1 * r) and A2: 0 <= r1 and A3: r1 <= 1 ; assume r in LSeg (p,q) ; ::_thesis: q = r then consider r2 being Real such that A4: r = ((1 - r2) * p) + (r2 * q) and 0 <= r2 and A5: r2 <= 1 ; A6: r1 * r2 <= 1 by A2, A3, A5, XREAL_1:160; A7: (1 - r2) + (r2 * (1 - r1)) = 1 - (r2 * r1) ; A8: r = ((1 - r2) * p) + ((r2 * ((1 - r1) * p)) + (r2 * (r1 * r))) by A1, A4, EUCLID:32 .= (((1 - r2) * p) + (r2 * ((1 - r1) * p))) + (r2 * (r1 * r)) by EUCLID:26 .= (((1 - r2) * p) + ((r2 * (1 - r1)) * p)) + (r2 * (r1 * r)) by EUCLID:30 .= ((1 - (r2 * r1)) * p) + (r2 * (r1 * r)) by A7, EUCLID:33 .= ((1 - (r2 * r1)) * p) + ((r2 * r1) * r) by EUCLID:30 ; A9: (1 - r1) + (r1 * (1 - r2)) = 1 - (r1 * r2) ; A10: q = ((1 - r1) * p) + ((r1 * ((1 - r2) * p)) + (r1 * (r2 * q))) by A1, A4, EUCLID:32 .= (((1 - r1) * p) + (r1 * ((1 - r2) * p))) + (r1 * (r2 * q)) by EUCLID:26 .= (((1 - r1) * p) + ((r1 * (1 - r2)) * p)) + (r1 * (r2 * q)) by EUCLID:30 .= ((1 - (r1 * r2)) * p) + (r1 * (r2 * q)) by A9, EUCLID:33 .= ((1 - (r1 * r2)) * p) + ((r1 * r2) * q) by EUCLID:30 ; percases ( r1 * r2 = 1 or r1 * r2 < 1 ) by A6, XXREAL_0:1; supposeA11: r1 * r2 = 1 ; ::_thesis: q = r then ( 1 <= r1 or 1 <= r2 ) by A2, XREAL_1:162; then ( 1 * r1 = 1 or 1 * r2 = 1 ) by A3, A5, XXREAL_0:1; hence q = (0 * p) + r by A1, A11, EUCLID:29 .= (0. (TOP-REAL n)) + r by EUCLID:29 .= r by EUCLID:27 ; ::_thesis: verum end; supposeA12: r1 * r2 < 1 ; ::_thesis: q = r hence q = p by A10, Th4 .= r by A8, A12, Th4 ; ::_thesis: verum end; end; end; begin theorem Th7: :: SPRECT_3:7 for A being non empty Subset of (TOP-REAL 2) for p being Element of (Euclid 2) for r being Real st A = Ball (p,r) holds A is connected proof let A be non empty Subset of (TOP-REAL 2); ::_thesis: for p being Element of (Euclid 2) for r being Real st A = Ball (p,r) holds A is connected let p be Element of (Euclid 2); ::_thesis: for r being Real st A = Ball (p,r) holds A is connected let r be Real; ::_thesis: ( A = Ball (p,r) implies A is connected ) assume A1: A = Ball (p,r) ; ::_thesis: A is connected A is convex proof let w1, w2 be Point of (TOP-REAL 2); :: according to JORDAN1:def_1 ::_thesis: ( not w1 in A or not w2 in A or LSeg (w1,w2) c= A ) assume that A2: w1 in A and A3: w2 in A ; ::_thesis: LSeg (w1,w2) c= A thus LSeg (w1,w2) c= A by A1, A2, A3, TOPREAL3:21; ::_thesis: verum end; hence A is connected ; ::_thesis: verum end; theorem Th8: :: SPRECT_3:8 for A, B being Subset of (TOP-REAL 2) st A is open & B is_a_component_of A holds B is open proof let A, B be Subset of (TOP-REAL 2); ::_thesis: ( A is open & B is_a_component_of A implies B is open ) assume that A1: A is open and A2: B is_a_component_of A ; ::_thesis: B is open A3: B c= A by A2, SPRECT_1:5; A4: TopStruct(# the U1 of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by EUCLID:def_8; then reconsider C = B, D = A as Subset of (TopSpaceMetr (Euclid 2)) ; A5: D is open by A1, A4, PRE_TOPC:30; for p being Point of (Euclid 2) st p in C holds ex r being real number st ( r > 0 & Ball (p,r) c= C ) proof let p be Point of (Euclid 2); ::_thesis: ( p in C implies ex r being real number st ( r > 0 & Ball (p,r) c= C ) ) assume A6: p in C ; ::_thesis: ex r being real number st ( r > 0 & Ball (p,r) c= C ) then consider r being real number such that A7: r > 0 and A8: Ball (p,r) c= D by A3, A5, TOPMETR:15; reconsider r = r as Real by XREAL_0:def_1; take r ; ::_thesis: ( r > 0 & Ball (p,r) c= C ) thus r > 0 by A7; ::_thesis: Ball (p,r) c= C reconsider E = Ball (p,r) as Subset of (TOP-REAL 2) by A4, TOPMETR:12; A9: p in E by A7, GOBOARD6:1; then A10: E is connected by Th7; B meets E by A6, A9, XBOOLE_0:3; hence Ball (p,r) c= C by A2, A8, A10, GOBOARD9:4; ::_thesis: verum end; then C is open by TOPMETR:15; hence B is open by A4, PRE_TOPC:30; ::_thesis: verum end; theorem :: SPRECT_3:9 for p, q, r, s being Point of (TOP-REAL 2) st LSeg (p,q) is horizontal & LSeg (r,s) is horizontal & LSeg (p,q) meets LSeg (r,s) holds p `2 = r `2 proof let p, q, r, s be Point of (TOP-REAL 2); ::_thesis: ( LSeg (p,q) is horizontal & LSeg (r,s) is horizontal & LSeg (p,q) meets LSeg (r,s) implies p `2 = r `2 ) assume that A1: LSeg (p,q) is horizontal and A2: LSeg (r,s) is horizontal ; ::_thesis: ( not LSeg (p,q) meets LSeg (r,s) or p `2 = r `2 ) assume LSeg (p,q) meets LSeg (r,s) ; ::_thesis: p `2 = r `2 then (LSeg (p,q)) /\ (LSeg (r,s)) <> {} by XBOOLE_0:def_7; then consider x being Point of (TOP-REAL 2) such that A3: x in (LSeg (p,q)) /\ (LSeg (r,s)) by SUBSET_1:4; A4: x in LSeg (r,s) by A3, XBOOLE_0:def_4; x in LSeg (p,q) by A3, XBOOLE_0:def_4; hence p `2 = x `2 by A1, SPPOL_1:40 .= r `2 by A2, A4, SPPOL_1:40 ; ::_thesis: verum end; theorem :: SPRECT_3:10 for p, q, r being Point of (TOP-REAL 2) st LSeg (p,q) is vertical & LSeg (q,r) is horizontal holds (LSeg (p,q)) /\ (LSeg (q,r)) = {q} proof let p, q, r be Point of (TOP-REAL 2); ::_thesis: ( LSeg (p,q) is vertical & LSeg (q,r) is horizontal implies (LSeg (p,q)) /\ (LSeg (q,r)) = {q} ) assume that A1: LSeg (p,q) is vertical and A2: LSeg (q,r) is horizontal ; ::_thesis: (LSeg (p,q)) /\ (LSeg (q,r)) = {q} for x being set holds ( x in (LSeg (p,q)) /\ (LSeg (q,r)) iff x = q ) proof let x be set ; ::_thesis: ( x in (LSeg (p,q)) /\ (LSeg (q,r)) iff x = q ) thus ( x in (LSeg (p,q)) /\ (LSeg (q,r)) implies x = q ) ::_thesis: ( x = q implies x in (LSeg (p,q)) /\ (LSeg (q,r)) ) proof assume A3: x in (LSeg (p,q)) /\ (LSeg (q,r)) ; ::_thesis: x = q then reconsider x = x as Point of (TOP-REAL 2) ; x in LSeg (q,r) by A3, XBOOLE_0:def_4; then A4: x `2 = q `2 by A2, SPPOL_1:40; x in LSeg (p,q) by A3, XBOOLE_0:def_4; then x `1 = q `1 by A1, SPPOL_1:41; hence x = q by A4, TOPREAL3:6; ::_thesis: verum end; assume A5: x = q ; ::_thesis: x in (LSeg (p,q)) /\ (LSeg (q,r)) then A6: x in LSeg (q,r) by RLTOPSP1:68; x in LSeg (p,q) by A5, RLTOPSP1:68; hence x in (LSeg (p,q)) /\ (LSeg (q,r)) by A6, XBOOLE_0:def_4; ::_thesis: verum end; hence (LSeg (p,q)) /\ (LSeg (q,r)) = {q} by TARSKI:def_1; ::_thesis: verum end; theorem :: SPRECT_3:11 for p, q, r, s being Point of (TOP-REAL 2) st LSeg (p,q) is horizontal & LSeg (s,r) is vertical & r in LSeg (p,q) holds (LSeg (p,q)) /\ (LSeg (s,r)) = {r} proof let p, q, r, s be Point of (TOP-REAL 2); ::_thesis: ( LSeg (p,q) is horizontal & LSeg (s,r) is vertical & r in LSeg (p,q) implies (LSeg (p,q)) /\ (LSeg (s,r)) = {r} ) assume that A1: LSeg (p,q) is horizontal and A2: LSeg (s,r) is vertical and A3: r in LSeg (p,q) ; ::_thesis: (LSeg (p,q)) /\ (LSeg (s,r)) = {r} for x being set holds ( x in (LSeg (p,q)) /\ (LSeg (s,r)) iff x = r ) proof let x be set ; ::_thesis: ( x in (LSeg (p,q)) /\ (LSeg (s,r)) iff x = r ) thus ( x in (LSeg (p,q)) /\ (LSeg (s,r)) implies x = r ) ::_thesis: ( x = r implies x in (LSeg (p,q)) /\ (LSeg (s,r)) ) proof assume A4: x in (LSeg (p,q)) /\ (LSeg (s,r)) ; ::_thesis: x = r then reconsider x = x as Point of (TOP-REAL 2) ; x in LSeg (p,q) by A4, XBOOLE_0:def_4; then A5: x `2 = p `2 by A1, SPPOL_1:40; x in LSeg (s,r) by A4, XBOOLE_0:def_4; then A6: x `1 = r `1 by A2, SPPOL_1:41; p `2 = r `2 by A1, A3, SPPOL_1:40; hence x = r by A5, A6, TOPREAL3:6; ::_thesis: verum end; assume A7: x = r ; ::_thesis: x in (LSeg (p,q)) /\ (LSeg (s,r)) then x in LSeg (s,r) by RLTOPSP1:68; hence x in (LSeg (p,q)) /\ (LSeg (s,r)) by A3, A7, XBOOLE_0:def_4; ::_thesis: verum end; hence (LSeg (p,q)) /\ (LSeg (s,r)) = {r} by TARSKI:def_1; ::_thesis: verum end; begin theorem :: SPRECT_3:12 for j, k, i being Element of NAT for G being Go-board st 1 <= j & j <= k & k <= width G & 1 <= i & i <= len G holds (G * (i,j)) `2 <= (G * (i,k)) `2 proof let j, k, i be Element of NAT ; ::_thesis: for G being Go-board st 1 <= j & j <= k & k <= width G & 1 <= i & i <= len G holds (G * (i,j)) `2 <= (G * (i,k)) `2 let G be Go-board; ::_thesis: ( 1 <= j & j <= k & k <= width G & 1 <= i & i <= len G implies (G * (i,j)) `2 <= (G * (i,k)) `2 ) assume that A1: 1 <= j and A2: j <= k and A3: k <= width G and A4: 1 <= i and A5: i <= len G ; ::_thesis: (G * (i,j)) `2 <= (G * (i,k)) `2 percases ( j < k or j = k ) by A2, XXREAL_0:1; suppose j < k ; ::_thesis: (G * (i,j)) `2 <= (G * (i,k)) `2 hence (G * (i,j)) `2 <= (G * (i,k)) `2 by A1, A3, A4, A5, GOBOARD5:4; ::_thesis: verum end; suppose j = k ; ::_thesis: (G * (i,j)) `2 <= (G * (i,k)) `2 hence (G * (i,j)) `2 <= (G * (i,k)) `2 ; ::_thesis: verum end; end; end; theorem :: SPRECT_3:13 for j, i, k being Element of NAT for G being Go-board st 1 <= j & j <= width G & 1 <= i & i <= k & k <= len G holds (G * (i,j)) `1 <= (G * (k,j)) `1 proof let j, i, k be Element of NAT ; ::_thesis: for G being Go-board st 1 <= j & j <= width G & 1 <= i & i <= k & k <= len G holds (G * (i,j)) `1 <= (G * (k,j)) `1 let G be Go-board; ::_thesis: ( 1 <= j & j <= width G & 1 <= i & i <= k & k <= len G implies (G * (i,j)) `1 <= (G * (k,j)) `1 ) assume that A1: 1 <= j and A2: j <= width G and A3: 1 <= i and A4: i <= k and A5: k <= len G ; ::_thesis: (G * (i,j)) `1 <= (G * (k,j)) `1 percases ( i < k or i = k ) by A4, XXREAL_0:1; suppose i < k ; ::_thesis: (G * (i,j)) `1 <= (G * (k,j)) `1 hence (G * (i,j)) `1 <= (G * (k,j)) `1 by A1, A2, A3, A5, GOBOARD5:3; ::_thesis: verum end; suppose i = k ; ::_thesis: (G * (i,j)) `1 <= (G * (k,j)) `1 hence (G * (i,j)) `1 <= (G * (k,j)) `1 ; ::_thesis: verum end; end; end; theorem Th14: :: SPRECT_3:14 for C being Subset of (TOP-REAL 2) holds LSeg ((NW-corner C),(NE-corner C)) c= L~ (SpStSeq C) proof let C be Subset of (TOP-REAL 2); ::_thesis: LSeg ((NW-corner C),(NE-corner C)) c= L~ (SpStSeq C) A1: (LSeg ((NW-corner C),(NE-corner C))) \/ (LSeg ((NE-corner C),(SE-corner C))) c= ((LSeg ((NW-corner C),(NE-corner C))) \/ (LSeg ((NE-corner C),(SE-corner C)))) \/ ((LSeg ((SE-corner C),(SW-corner C))) \/ (LSeg ((SW-corner C),(NW-corner C)))) by XBOOLE_1:7; LSeg ((NW-corner C),(NE-corner C)) c= (LSeg ((NW-corner C),(NE-corner C))) \/ (LSeg ((NE-corner C),(SE-corner C))) by XBOOLE_1:7; then LSeg ((NW-corner C),(NE-corner C)) c= ((LSeg ((NW-corner C),(NE-corner C))) \/ (LSeg ((NE-corner C),(SE-corner C)))) \/ ((LSeg ((SE-corner C),(SW-corner C))) \/ (LSeg ((SW-corner C),(NW-corner C)))) by A1, XBOOLE_1:1; hence LSeg ((NW-corner C),(NE-corner C)) c= L~ (SpStSeq C) by SPRECT_1:41; ::_thesis: verum end; theorem Th15: :: SPRECT_3:15 for C being non empty compact Subset of (TOP-REAL 2) holds N-min C in LSeg ((NW-corner C),(NE-corner C)) proof let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: N-min C in LSeg ((NW-corner C),(NE-corner C)) A1: N-most C c= LSeg ((NW-corner C),(NE-corner C)) by XBOOLE_1:17; N-min C in N-most C by PSCOMP_1:42; hence N-min C in LSeg ((NW-corner C),(NE-corner C)) by A1; ::_thesis: verum end; registration let C be Subset of (TOP-REAL 2); cluster LSeg ((NW-corner C),(NE-corner C)) -> horizontal ; coherence LSeg ((NW-corner C),(NE-corner C)) is horizontal proof (NW-corner C) `2 = N-bound C by EUCLID:52 .= (NE-corner C) `2 by EUCLID:52 ; hence LSeg ((NW-corner C),(NE-corner C)) is horizontal by SPPOL_1:15; ::_thesis: verum end; end; theorem :: SPRECT_3:16 for g being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st g /. 1 <> p & ( (g /. 1) `1 = p `1 or (g /. 1) `2 = p `2 ) & g is being_S-Seq & (LSeg (p,(g /. 1))) /\ (L~ g) = {(g /. 1)} holds <*p*> ^ g is being_S-Seq proof let g be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st g /. 1 <> p & ( (g /. 1) `1 = p `1 or (g /. 1) `2 = p `2 ) & g is being_S-Seq & (LSeg (p,(g /. 1))) /\ (L~ g) = {(g /. 1)} holds <*p*> ^ g is being_S-Seq let p be Point of (TOP-REAL 2); ::_thesis: ( g /. 1 <> p & ( (g /. 1) `1 = p `1 or (g /. 1) `2 = p `2 ) & g is being_S-Seq & (LSeg (p,(g /. 1))) /\ (L~ g) = {(g /. 1)} implies <*p*> ^ g is being_S-Seq ) assume that A1: g /. 1 <> p and A2: ( (g /. 1) `1 = p `1 or (g /. 1) `2 = p `2 ) and A3: g is being_S-Seq and A4: (LSeg (p,(g /. 1))) /\ (L~ g) = {(g /. 1)} ; ::_thesis: <*p*> ^ g is being_S-Seq set f = <*p,(g /. 1)*>; A5: <*p,(g /. 1)*> is being_S-Seq by A1, A2, SPPOL_2:43; reconsider g9 = g as S-Sequence_in_R2 by A3; A6: 1 in dom g9 by FINSEQ_5:6; A7: len <*p,(g /. 1)*> = 1 + 1 by FINSEQ_1:44; then (len <*p,(g /. 1)*>) -' 1 = 1 by NAT_D:34; then A8: mid (<*p,(g /. 1)*>,1,((len <*p,(g /. 1)*>) -' 1)) = <*(<*p,(g /. 1)*> /. 1)*> by A7, JORDAN4:15 .= <*p*> by FINSEQ_4:17 ; A9: (L~ <*p,(g /. 1)*>) /\ (L~ g) = {(g /. 1)} by A4, SPPOL_2:21 .= {(g . 1)} by A6, PARTFUN1:def_6 ; <*p,(g /. 1)*> . (len <*p,(g /. 1)*>) = g /. 1 by A7, FINSEQ_1:44 .= g . 1 by A6, PARTFUN1:def_6 ; hence <*p*> ^ g is being_S-Seq by A3, A5, A9, A8, JORDAN3:45; ::_thesis: verum end; theorem :: SPRECT_3:17 for j being Element of NAT for f being S-Sequence_in_R2 for p being Point of (TOP-REAL 2) st 1 < j & j <= len f & p in L~ (mid (f,1,j)) holds LE p,f /. j, L~ f,f /. 1,f /. (len f) proof let j be Element of NAT ; ::_thesis: for f being S-Sequence_in_R2 for p being Point of (TOP-REAL 2) st 1 < j & j <= len f & p in L~ (mid (f,1,j)) holds LE p,f /. j, L~ f,f /. 1,f /. (len f) let f be S-Sequence_in_R2; ::_thesis: for p being Point of (TOP-REAL 2) st 1 < j & j <= len f & p in L~ (mid (f,1,j)) holds LE p,f /. j, L~ f,f /. 1,f /. (len f) let p be Point of (TOP-REAL 2); ::_thesis: ( 1 < j & j <= len f & p in L~ (mid (f,1,j)) implies LE p,f /. j, L~ f,f /. 1,f /. (len f) ) assume that A1: 1 < j and A2: j <= len f and A3: p in L~ (mid (f,1,j)) ; ::_thesis: LE p,f /. j, L~ f,f /. 1,f /. (len f) consider i being Element of NAT such that A4: 1 <= i and A5: i + 1 <= len (mid (f,1,j)) and A6: p in LSeg ((mid (f,1,j)),i) by A3, SPPOL_2:13; A7: (j -' 1) + 1 = j by A1, XREAL_1:235; then A8: i + 1 <= j by A1, A2, A5, JORDAN4:8; then i < (j -' 1) + 1 by A7, NAT_1:13; then A9: LSeg ((mid (f,1,j)),i) = LSeg (f,((i + 1) -' 1)) by A1, A2, A4, JORDAN4:19; 1 <= i + 1 by NAT_1:11; then A10: LE f /. (i + 1),f /. j, L~ f,f /. 1,f /. (len f) by A2, A8, JORDAN5C:24; A11: i = (i + 1) -' 1 by NAT_D:34; i + 1 <= len f by A2, A8, XXREAL_0:2; then LE p,f /. (i + 1), L~ f,f /. 1,f /. (len f) by A4, A6, A11, A9, JORDAN5C:26; hence LE p,f /. j, L~ f,f /. 1,f /. (len f) by A10, JORDAN5C:13; ::_thesis: verum end; theorem :: SPRECT_3:18 for i, j being Element of NAT for h being FinSequence of (TOP-REAL 2) st i in dom h & j in dom h holds L~ (mid (h,i,j)) c= L~ h proof let i, j be Element of NAT ; ::_thesis: for h being FinSequence of (TOP-REAL 2) st i in dom h & j in dom h holds L~ (mid (h,i,j)) c= L~ h let h be FinSequence of (TOP-REAL 2); ::_thesis: ( i in dom h & j in dom h implies L~ (mid (h,i,j)) c= L~ h ) assume that A1: i in dom h and A2: j in dom h ; ::_thesis: L~ (mid (h,i,j)) c= L~ h A3: i <= len h by A1, FINSEQ_3:25; A4: j <= len h by A2, FINSEQ_3:25; A5: 1 <= j by A2, FINSEQ_3:25; 1 <= i by A1, FINSEQ_3:25; hence L~ (mid (h,i,j)) c= L~ h by A3, A5, A4, JORDAN4:35; ::_thesis: verum end; theorem :: SPRECT_3:19 for i, j being Element of NAT st 1 <= i & i < j holds for f being FinSequence of (TOP-REAL 2) st j <= len f holds L~ (mid (f,i,j)) = (LSeg (f,i)) \/ (L~ (mid (f,(i + 1),j))) proof let i, j be Element of NAT ; ::_thesis: ( 1 <= i & i < j implies for f being FinSequence of (TOP-REAL 2) st j <= len f holds L~ (mid (f,i,j)) = (LSeg (f,i)) \/ (L~ (mid (f,(i + 1),j))) ) assume that A1: 1 <= i and A2: i < j ; ::_thesis: for f being FinSequence of (TOP-REAL 2) st j <= len f holds L~ (mid (f,i,j)) = (LSeg (f,i)) \/ (L~ (mid (f,(i + 1),j))) let f be FinSequence of (TOP-REAL 2); ::_thesis: ( j <= len f implies L~ (mid (f,i,j)) = (LSeg (f,i)) \/ (L~ (mid (f,(i + 1),j))) ) assume A3: j <= len f ; ::_thesis: L~ (mid (f,i,j)) = (LSeg (f,i)) \/ (L~ (mid (f,(i + 1),j))) set A = { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } ; set B = { (LSeg (f,k)) where k is Element of NAT : ( i + 1 <= k & k < j ) } ; A4: { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } = { (LSeg (f,k)) where k is Element of NAT : ( i + 1 <= k & k < j ) } \/ {(LSeg (f,i))} proof thus { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } c= { (LSeg (f,k)) where k is Element of NAT : ( i + 1 <= k & k < j ) } \/ {(LSeg (f,i))} :: according to XBOOLE_0:def_10 ::_thesis: { (LSeg (f,k)) where k is Element of NAT : ( i + 1 <= k & k < j ) } \/ {(LSeg (f,i))} c= { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } or e in { (LSeg (f,k)) where k is Element of NAT : ( i + 1 <= k & k < j ) } \/ {(LSeg (f,i))} ) assume e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } ; ::_thesis: e in { (LSeg (f,k)) where k is Element of NAT : ( i + 1 <= k & k < j ) } \/ {(LSeg (f,i))} then consider k being Element of NAT such that A5: e = LSeg (f,k) and A6: i <= k and A7: k < j ; ( i = k or i < k ) by A6, XXREAL_0:1; then ( i = k or i + 1 <= k ) by NAT_1:13; then ( e in { (LSeg (f,k)) where k is Element of NAT : ( i + 1 <= k & k < j ) } or e in {(LSeg (f,i))} ) by A5, A7, TARSKI:def_1; hence e in { (LSeg (f,k)) where k is Element of NAT : ( i + 1 <= k & k < j ) } \/ {(LSeg (f,i))} by XBOOLE_0:def_3; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (LSeg (f,k)) where k is Element of NAT : ( i + 1 <= k & k < j ) } \/ {(LSeg (f,i))} or e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } ) assume A8: e in { (LSeg (f,k)) where k is Element of NAT : ( i + 1 <= k & k < j ) } \/ {(LSeg (f,i))} ; ::_thesis: e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } percases ( e in { (LSeg (f,k)) where k is Element of NAT : ( i + 1 <= k & k < j ) } or e in {(LSeg (f,i))} ) by A8, XBOOLE_0:def_3; suppose e in { (LSeg (f,k)) where k is Element of NAT : ( i + 1 <= k & k < j ) } ; ::_thesis: e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } then consider k being Element of NAT such that A9: e = LSeg (f,k) and A10: i + 1 <= k and A11: k < j ; i < k by A10, NAT_1:13; hence e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } by A9, A11; ::_thesis: verum end; suppose e in {(LSeg (f,i))} ; ::_thesis: e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } then e = LSeg (f,i) by TARSKI:def_1; hence e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } by A2; ::_thesis: verum end; end; end; A12: 1 <= i + 1 by NAT_1:11; A13: i + 1 <= j by A2, NAT_1:13; thus L~ (mid (f,i,j)) = union { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } by A1, A2, A3, SPRECT_2:14 .= (union { (LSeg (f,k)) where k is Element of NAT : ( i + 1 <= k & k < j ) } ) \/ (union {(LSeg (f,i))}) by A4, ZFMISC_1:78 .= (union { (LSeg (f,k)) where k is Element of NAT : ( i + 1 <= k & k < j ) } ) \/ (LSeg (f,i)) by ZFMISC_1:25 .= (LSeg (f,i)) \/ (L~ (mid (f,(i + 1),j))) by A3, A12, A13, SPRECT_2:14 ; ::_thesis: verum end; theorem :: SPRECT_3:20 for i, j being Element of NAT for f being FinSequence of (TOP-REAL 2) st 1 <= i & i < j & j <= len f holds L~ (mid (f,i,j)) = (L~ (mid (f,i,(j -' 1)))) \/ (LSeg (f,(j -' 1))) proof let i, j be Element of NAT ; ::_thesis: for f being FinSequence of (TOP-REAL 2) st 1 <= i & i < j & j <= len f holds L~ (mid (f,i,j)) = (L~ (mid (f,i,(j -' 1)))) \/ (LSeg (f,(j -' 1))) let f be FinSequence of (TOP-REAL 2); ::_thesis: ( 1 <= i & i < j & j <= len f implies L~ (mid (f,i,j)) = (L~ (mid (f,i,(j -' 1)))) \/ (LSeg (f,(j -' 1))) ) assume that A1: 1 <= i and A2: i < j and A3: j <= len f ; ::_thesis: L~ (mid (f,i,j)) = (L~ (mid (f,i,(j -' 1)))) \/ (LSeg (f,(j -' 1))) j -' 1 <= j by NAT_D:35; then A4: j -' 1 <= len f by A3, XXREAL_0:2; set A = { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } ; set B = { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j -' 1 ) } ; A5: i <= j -' 1 by A2, NAT_D:49; A6: { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } = { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j -' 1 ) } \/ {(LSeg (f,(j -' 1)))} proof thus { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } c= { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j -' 1 ) } \/ {(LSeg (f,(j -' 1)))} :: according to XBOOLE_0:def_10 ::_thesis: { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j -' 1 ) } \/ {(LSeg (f,(j -' 1)))} c= { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } or e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j -' 1 ) } \/ {(LSeg (f,(j -' 1)))} ) assume e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } ; ::_thesis: e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j -' 1 ) } \/ {(LSeg (f,(j -' 1)))} then consider k being Element of NAT such that A7: e = LSeg (f,k) and A8: i <= k and A9: k < j ; k <= j -' 1 by A9, NAT_D:49; then ( j -' 1 = k or k < j -' 1 ) by XXREAL_0:1; then ( e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j -' 1 ) } or e in {(LSeg (f,(j -' 1)))} ) by A7, A8, TARSKI:def_1; hence e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j -' 1 ) } \/ {(LSeg (f,(j -' 1)))} by XBOOLE_0:def_3; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j -' 1 ) } \/ {(LSeg (f,(j -' 1)))} or e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } ) A10: j -' 1 <= j by NAT_D:35; assume A11: e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j -' 1 ) } \/ {(LSeg (f,(j -' 1)))} ; ::_thesis: e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } percases ( e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j -' 1 ) } or e in {(LSeg (f,(j -' 1)))} ) by A11, XBOOLE_0:def_3; suppose e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j -' 1 ) } ; ::_thesis: e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } then consider k being Element of NAT such that A12: e = LSeg (f,k) and A13: i <= k and A14: k < j -' 1 ; k < j by A10, A14, XXREAL_0:2; hence e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } by A12, A13; ::_thesis: verum end; supposeA15: e in {(LSeg (f,(j -' 1)))} ; ::_thesis: e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } 1 <= j -' 1 by A1, A5, XXREAL_0:2; then A16: j -' 1 < j by NAT_D:51; e = LSeg (f,(j -' 1)) by A15, TARSKI:def_1; hence e in { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } by A5, A16; ::_thesis: verum end; end; end; thus L~ (mid (f,i,j)) = union { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j ) } by A1, A2, A3, SPRECT_2:14 .= (union { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j -' 1 ) } ) \/ (union {(LSeg (f,(j -' 1)))}) by A6, ZFMISC_1:78 .= (union { (LSeg (f,k)) where k is Element of NAT : ( i <= k & k < j -' 1 ) } ) \/ (LSeg (f,(j -' 1))) by ZFMISC_1:25 .= (L~ (mid (f,i,(j -' 1)))) \/ (LSeg (f,(j -' 1))) by A1, A5, A4, SPRECT_2:14 ; ::_thesis: verum end; theorem :: SPRECT_3:21 for f, g being FinSequence of (TOP-REAL 2) st f is being_S-Seq & g is being_S-Seq & ( (f /. (len f)) `1 = (g /. 1) `1 or (f /. (len f)) `2 = (g /. 1) `2 ) & L~ f misses L~ g & (LSeg ((f /. (len f)),(g /. 1))) /\ (L~ f) = {(f /. (len f))} & (LSeg ((f /. (len f)),(g /. 1))) /\ (L~ g) = {(g /. 1)} holds f ^ g is being_S-Seq proof let f, g be FinSequence of (TOP-REAL 2); ::_thesis: ( f is being_S-Seq & g is being_S-Seq & ( (f /. (len f)) `1 = (g /. 1) `1 or (f /. (len f)) `2 = (g /. 1) `2 ) & L~ f misses L~ g & (LSeg ((f /. (len f)),(g /. 1))) /\ (L~ f) = {(f /. (len f))} & (LSeg ((f /. (len f)),(g /. 1))) /\ (L~ g) = {(g /. 1)} implies f ^ g is being_S-Seq ) assume that A1: f is being_S-Seq and A2: g is being_S-Seq and A3: ( (f /. (len f)) `1 = (g /. 1) `1 or (f /. (len f)) `2 = (g /. 1) `2 ) and A4: L~ f misses L~ g and A5: (LSeg ((f /. (len f)),(g /. 1))) /\ (L~ f) = {(f /. (len f))} and A6: (LSeg ((f /. (len f)),(g /. 1))) /\ (L~ g) = {(g /. 1)} ; ::_thesis: f ^ g is being_S-Seq A7: len g >= 2 by A2, TOPREAL1:def_8; then A8: len g >= 1 by XXREAL_0:2; then 1 in dom g by FINSEQ_3:25; then A9: g /. 1 in L~ g by A7, GOBOARD1:1; set h = <*(f /. (len f))*> ^ g; A10: len f >= 2 by A1, TOPREAL1:def_8; then 1 <= len f by XXREAL_0:2; then A11: len f in dom f by FINSEQ_3:25; then A12: f . (len f) = f /. (len f) by PARTFUN1:def_6 .= (<*(f /. (len f))*> ^ g) . 1 by FINSEQ_1:41 ; A13: len (<*(f /. (len f))*> ^ g) = (len <*(f /. (len f))*>) + (len g) by FINSEQ_1:22 .= (len g) + 1 by FINSEQ_1:39 ; then len (<*(f /. (len f))*> ^ g) >= 1 + 1 by A8, XREAL_1:6; then A14: mid ((<*(f /. (len f))*> ^ g),2,(len (<*(f /. (len f))*> ^ g))) = ((<*(f /. (len f))*> ^ g) /^ ((1 + 1) -' 1)) | (((len (<*(f /. (len f))*> ^ g)) -' 2) + 1) by FINSEQ_6:def_3 .= ((<*(f /. (len f))*> ^ g) /^ 1) | (((len (<*(f /. (len f))*> ^ g)) -' 2) + 1) by NAT_D:34 .= g | (((len (<*(f /. (len f))*> ^ g)) -' 2) + 1) by FINSEQ_6:45 .= g | ((((len (<*(f /. (len f))*> ^ g)) -' 1) -' 1) + 1) by NAT_D:45 .= g | (((len g) -' 1) + 1) by A13, NAT_D:34 .= g | (len g) by A7, XREAL_1:235, XXREAL_0:2 .= g by FINSEQ_1:58 ; f /. (len f) in L~ f by A10, A11, GOBOARD1:1; then f /. (len f) <> g /. 1 by A4, A9, XBOOLE_0:3; then A15: <*(f /. (len f))*> ^ g is being_S-Seq by A2, A3, A6, SPRECT_2:60; (L~ f) /\ (L~ (<*(f /. (len f))*> ^ g)) = (L~ f) /\ ((LSeg ((f /. (len f)),(g /. 1))) \/ (L~ g)) by A2, SPPOL_2:20 .= ((L~ f) /\ (LSeg ((f /. (len f)),(g /. 1)))) \/ ((L~ f) /\ (L~ g)) by XBOOLE_1:23 .= ((L~ f) /\ (LSeg ((f /. (len f)),(g /. 1)))) \/ {} by A4, XBOOLE_0:def_7 .= {((<*(f /. (len f))*> ^ g) . 1)} by A5, A11, A12, PARTFUN1:def_6 ; hence f ^ g is being_S-Seq by A1, A12, A15, A14, JORDAN3:38; ::_thesis: verum end; theorem :: SPRECT_3:22 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in L~ f holds (R_Cut (f,p)) /. 1 = f /. 1 proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st p in L~ f holds (R_Cut (f,p)) /. 1 = f /. 1 let p be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f implies (R_Cut (f,p)) /. 1 = f /. 1 ) set i = Index (p,f); assume A1: p in L~ f ; ::_thesis: (R_Cut (f,p)) /. 1 = f /. 1 then A2: 1 <= Index (p,f) by JORDAN3:8; Index (p,f) <= len f by A1, JORDAN3:8; then f <> {} by A2; then A3: 1 in dom f by FINSEQ_5:6; ( p = f . 1 or p <> f . 1 ) ; then ( len (R_Cut (f,p)) = Index (p,f) or len (R_Cut (f,p)) = (Index (p,f)) + 1 ) by A1, JORDAN3:25; then 1 <= len (R_Cut (f,p)) by A1, JORDAN3:8, NAT_1:11; hence (R_Cut (f,p)) /. 1 = (R_Cut (f,p)) . 1 by FINSEQ_4:15 .= f . 1 by A1, A2, JORDAN3:24 .= f /. 1 by A3, PARTFUN1:def_6 ; ::_thesis: verum end; theorem :: SPRECT_3:23 for j being Element of NAT for f being S-Sequence_in_R2 for p, q being Point of (TOP-REAL 2) st 1 <= j & j < len f & p in LSeg (f,j) & q in LSeg ((f /. j),p) holds LE q,p, L~ f,f /. 1,f /. (len f) proof let j be Element of NAT ; ::_thesis: for f being S-Sequence_in_R2 for p, q being Point of (TOP-REAL 2) st 1 <= j & j < len f & p in LSeg (f,j) & q in LSeg ((f /. j),p) holds LE q,p, L~ f,f /. 1,f /. (len f) let f be S-Sequence_in_R2; ::_thesis: for p, q being Point of (TOP-REAL 2) st 1 <= j & j < len f & p in LSeg (f,j) & q in LSeg ((f /. j),p) holds LE q,p, L~ f,f /. 1,f /. (len f) let p, q be Point of (TOP-REAL 2); ::_thesis: ( 1 <= j & j < len f & p in LSeg (f,j) & q in LSeg ((f /. j),p) implies LE q,p, L~ f,f /. 1,f /. (len f) ) assume that A1: 1 <= j and A2: j < len f and A3: p in LSeg (f,j) and A4: q in LSeg ((f /. j),p) ; ::_thesis: LE q,p, L~ f,f /. 1,f /. (len f) A5: j + 1 <= len f by A2, NAT_1:13; then A6: LSeg (f,j) = LSeg ((f /. j),(f /. (j + 1))) by A1, TOPREAL1:def_3; A7: f /. j in LSeg (f,j) by A1, A5, TOPREAL1:21; then A8: LSeg ((f /. j),p) c= LSeg (f,j) by A3, A6, TOPREAL1:6; then A9: q in LSeg (f,j) by A4; A10: LSeg (f,j) c= L~ f by TOPREAL3:19; percases ( p = q or q <> p ) ; suppose p = q ; ::_thesis: LE q,p, L~ f,f /. 1,f /. (len f) hence LE q,p, L~ f,f /. 1,f /. (len f) by A3, A10, JORDAN5C:9; ::_thesis: verum end; supposeA11: q <> p ; ::_thesis: LE q,p, L~ f,f /. 1,f /. (len f) for i, j being Element of NAT st q in LSeg (f,i) & p in LSeg (f,j) & 1 <= i & i + 1 <= len f & 1 <= j & j + 1 <= len f holds ( i <= j & ( i = j implies LE q,p,f /. i,f /. (i + 1) ) ) proof 1 <= j + 1 by NAT_1:11; then A12: j + 1 in dom f by A5, FINSEQ_3:25; let i1, i2 be Element of NAT ; ::_thesis: ( q in LSeg (f,i1) & p in LSeg (f,i2) & 1 <= i1 & i1 + 1 <= len f & 1 <= i2 & i2 + 1 <= len f implies ( i1 <= i2 & ( i1 = i2 implies LE q,p,f /. i1,f /. (i1 + 1) ) ) ) assume that A13: q in LSeg (f,i1) and A14: p in LSeg (f,i2) and 1 <= i1 and A15: i1 + 1 <= len f and A16: 1 <= i2 and i2 + 1 <= len f ; ::_thesis: ( i1 <= i2 & ( i1 = i2 implies LE q,p,f /. i1,f /. (i1 + 1) ) ) A17: p in (LSeg (f,i2)) /\ (LSeg (f,j)) by A3, A14, XBOOLE_0:def_4; then A18: LSeg (f,i2) meets LSeg (f,j) by XBOOLE_0:4; then A19: j + 1 >= i2 by TOPREAL1:def_7; A20: q in (LSeg (f,i1)) /\ (LSeg (f,j)) by A4, A8, A13, XBOOLE_0:def_4; then A21: LSeg (f,i1) meets LSeg (f,j) by XBOOLE_0:4; then A22: i1 + 1 >= j by TOPREAL1:def_7; A23: now__::_thesis:_not_i2_+_1_=_j assume A24: i2 + 1 = j ; ::_thesis: contradiction i2 + (1 + 1) = (i2 + 1) + 1 ; then i2 + 2 <= len f by A2, A24, NAT_1:13; then p in {(f /. j)} by A16, A17, A24, TOPREAL1:def_6; then p = f /. j by TARSKI:def_1; then q in {p} by A4, RLTOPSP1:70; hence contradiction by A11, TARSKI:def_1; ::_thesis: verum end; A25: now__::_thesis:_(_i2_+_1_>_j_&_j_+_1_>_i2_implies_i2_=_j_) assume that A26: i2 + 1 > j and A27: j + 1 > i2 ; ::_thesis: i2 = j A28: j <= i2 by A26, NAT_1:13; i2 <= j by A27, NAT_1:13; hence i2 = j by A28, XXREAL_0:1; ::_thesis: verum end; i2 + 1 >= j by A18, TOPREAL1:def_7; then ( i2 + 1 = j or i2 = j or j + 1 = i2 ) by A25, A19, XXREAL_0:1; then A29: i2 >= j by A23, NAT_1:11; A30: now__::_thesis:_(_i1_+_1_>_j_&_j_+_1_>_i1_implies_i1_=_j_) assume that A31: i1 + 1 > j and A32: j + 1 > i1 ; ::_thesis: i1 = j A33: j <= i1 by A31, NAT_1:13; i1 <= j by A32, NAT_1:13; hence i1 = j by A33, XXREAL_0:1; ::_thesis: verum end; A34: j in dom f by A1, A2, FINSEQ_3:25; A35: now__::_thesis:_not_f_/._(j_+_1)_=_f_/._j assume f /. (j + 1) = f /. j ; ::_thesis: contradiction then j = j + 1 by A12, A34, PARTFUN2:10; hence contradiction ; ::_thesis: verum end; A36: now__::_thesis:_not_i1_=_j_+_1 A37: j + (1 + 1) = (j + 1) + 1 ; assume i1 = j + 1 ; ::_thesis: contradiction then q in {(f /. (j + 1))} by A1, A15, A20, A37, TOPREAL1:def_6; then q = f /. (j + 1) by TARSKI:def_1; hence contradiction by A3, A4, A6, A7, A11, A35, SPPOL_1:7, TOPREAL1:6; ::_thesis: verum end; A38: j + 1 >= i1 by A21, TOPREAL1:def_7; then ( i1 + 1 = j or i1 = j or j + 1 = i1 ) by A30, A22, XXREAL_0:1; then i1 <= j by A36, NAT_1:11; hence i1 <= i2 by A29, XXREAL_0:2; ::_thesis: ( i1 = i2 implies LE q,p,f /. i1,f /. (i1 + 1) ) assume A39: i1 = i2 ; ::_thesis: LE q,p,f /. i1,f /. (i1 + 1) not p in LSeg ((f /. j),q) by A4, A11, Th6; then not LE p,q,f /. j,f /. (j + 1) by JORDAN3:30; then LT q,p,f /. j,f /. (j + 1) by A3, A6, A13, A23, A30, A22, A38, A35, A36, A39, JORDAN3:28, XXREAL_0:1; hence LE q,p,f /. i1,f /. (i1 + 1) by A23, A30, A22, A38, A36, A39, JORDAN3:def_6, XXREAL_0:1; ::_thesis: verum end; hence LE q,p, L~ f,f /. 1,f /. (len f) by A3, A9, A10, A11, JORDAN5C:30; ::_thesis: verum end; end; end; begin theorem Th24: :: SPRECT_3:24 for f being non constant standard special_circular_sequence holds ( LeftComp f is open & RightComp f is open ) proof let f be non constant standard special_circular_sequence; ::_thesis: ( LeftComp f is open & RightComp f is open ) LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def_1; hence LeftComp f is open by Th8; ::_thesis: RightComp f is open RightComp f is_a_component_of (L~ f) ` by GOBOARD9:def_2; hence RightComp f is open by Th8; ::_thesis: verum end; registration let f be non constant standard special_circular_sequence; cluster L~ f -> non horizontal non vertical ; coherence ( not L~ f is vertical & not L~ f is horizontal ) proof W-bound (L~ f) <> E-bound (L~ f) by TOPREAL5:17; hence not L~ f is vertical by SPRECT_1:15; ::_thesis: not L~ f is horizontal S-bound (L~ f) <> N-bound (L~ f) by TOPREAL5:16; hence not L~ f is horizontal by SPRECT_1:16; ::_thesis: verum end; cluster LeftComp f -> being_Region ; coherence LeftComp f is being_Region proof thus LeftComp f is open by Th24; :: according to TOPREAL4:def_3 ::_thesis: LeftComp f is connected LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def_1; then consider A being Subset of ((TOP-REAL 2) | ((L~ f) `)) such that A1: A = LeftComp f and A2: A is a_component by CONNSP_1:def_6; A is connected by A2, CONNSP_1:def_5; hence LeftComp f is connected by A1, CONNSP_1:23; ::_thesis: verum end; cluster RightComp f -> being_Region ; coherence RightComp f is being_Region proof thus RightComp f is open by Th24; :: according to TOPREAL4:def_3 ::_thesis: RightComp f is connected RightComp f is_a_component_of (L~ f) ` by GOBOARD9:def_2; then consider A being Subset of ((TOP-REAL 2) | ((L~ f) `)) such that A3: A = RightComp f and A4: A is a_component by CONNSP_1:def_6; A is connected by A4, CONNSP_1:def_5; hence RightComp f is connected by A3, CONNSP_1:23; ::_thesis: verum end; end; theorem Th25: :: SPRECT_3:25 for f being non constant standard special_circular_sequence holds RightComp f misses L~ f proof let f be non constant standard special_circular_sequence; ::_thesis: RightComp f misses L~ f (L~ f) ` = (LeftComp f) \/ (RightComp f) by GOBRD12:10; then RightComp f c= (L~ f) ` by XBOOLE_1:7; hence RightComp f misses L~ f by SUBSET_1:23; ::_thesis: verum end; theorem Th26: :: SPRECT_3:26 for f being non constant standard special_circular_sequence holds LeftComp f misses L~ f proof let f be non constant standard special_circular_sequence; ::_thesis: LeftComp f misses L~ f (L~ f) ` = (LeftComp f) \/ (RightComp f) by GOBRD12:10; then LeftComp f c= (L~ f) ` by XBOOLE_1:7; hence LeftComp f misses L~ f by SUBSET_1:23; ::_thesis: verum end; theorem Th27: :: SPRECT_3:27 for f being non constant standard special_circular_sequence holds i_w_n f < i_e_n f proof let f be non constant standard special_circular_sequence; ::_thesis: i_w_n f < i_e_n f set G = GoB f; A1: i_w_n f <= len (GoB f) by JORDAN5D:45; A2: (GoB f) * ((i_w_n f),(width (GoB f))) = N-min (L~ f) by JORDAN5D:def_7; assume A3: i_w_n f >= i_e_n f ; ::_thesis: contradiction A4: 1 <= i_e_n f by JORDAN5D:45; A5: (N-min (L~ f)) `1 < (N-max (L~ f)) `1 by SPRECT_2:51; A6: (GoB f) * ((i_e_n f),(width (GoB f))) = N-max (L~ f) by JORDAN5D:def_8; then i_w_n f <> i_e_n f by A5, JORDAN5D:def_7; then A7: i_w_n f > i_e_n f by A3, XXREAL_0:1; width (GoB f) > 1 by GOBOARD7:33; hence contradiction by A1, A2, A4, A6, A5, A7, GOBOARD5:3; ::_thesis: verum end; theorem Th28: :: SPRECT_3:28 for f being non constant standard special_circular_sequence ex i being Element of NAT st ( 1 <= i & i < len (GoB f) & N-min (L~ f) = (GoB f) * (i,(width (GoB f))) ) proof let f be non constant standard special_circular_sequence; ::_thesis: ex i being Element of NAT st ( 1 <= i & i < len (GoB f) & N-min (L~ f) = (GoB f) * (i,(width (GoB f))) ) take i = i_w_n f; ::_thesis: ( 1 <= i & i < len (GoB f) & N-min (L~ f) = (GoB f) * (i,(width (GoB f))) ) thus 1 <= i by JORDAN5D:45; ::_thesis: ( i < len (GoB f) & N-min (L~ f) = (GoB f) * (i,(width (GoB f))) ) i_e_n f <= len (GoB f) by JORDAN5D:45; hence i < len (GoB f) by Th27, XXREAL_0:2; ::_thesis: N-min (L~ f) = (GoB f) * (i,(width (GoB f))) thus N-min (L~ f) = (GoB f) * (i,(width (GoB f))) by JORDAN5D:def_7; ::_thesis: verum end; theorem Th29: :: SPRECT_3:29 for i being Element of NAT for f being non constant standard clockwise_oriented special_circular_sequence st i in dom (GoB f) & f /. 1 = (GoB f) * (i,(width (GoB f))) & f /. 1 = N-min (L~ f) holds ( f /. 2 = (GoB f) * ((i + 1),(width (GoB f))) & f /. ((len f) -' 1) = (GoB f) * (i,((width (GoB f)) -' 1)) ) proof let i be Element of NAT ; ::_thesis: for f being non constant standard clockwise_oriented special_circular_sequence st i in dom (GoB f) & f /. 1 = (GoB f) * (i,(width (GoB f))) & f /. 1 = N-min (L~ f) holds ( f /. 2 = (GoB f) * ((i + 1),(width (GoB f))) & f /. ((len f) -' 1) = (GoB f) * (i,((width (GoB f)) -' 1)) ) let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( i in dom (GoB f) & f /. 1 = (GoB f) * (i,(width (GoB f))) & f /. 1 = N-min (L~ f) implies ( f /. 2 = (GoB f) * ((i + 1),(width (GoB f))) & f /. ((len f) -' 1) = (GoB f) * (i,((width (GoB f)) -' 1)) ) ) assume that A1: i in dom (GoB f) and A2: f /. 1 = (GoB f) * (i,(width (GoB f))) and A3: f /. 1 = N-min (L~ f) ; ::_thesis: ( f /. 2 = (GoB f) * ((i + 1),(width (GoB f))) & f /. ((len f) -' 1) = (GoB f) * (i,((width (GoB f)) -' 1)) ) A4: i <= len (GoB f) by A1, FINSEQ_3:25; 4 < len f by GOBOARD7:34; then A5: ((len f) -' 1) + 1 = len f by XREAL_1:235, XXREAL_0:2; A6: f /. (len f) = f /. 1 by FINSEQ_6:def_1; A7: 1 <= len f by GOBOARD7:34, XXREAL_0:2; then A8: 1 in dom f by FINSEQ_3:25; A9: 1 <= width (GoB f) by GOBRD11:34; A10: f /. 2 in N-most (L~ f) by A3, SPRECT_2:30; A11: 1 + 1 <= len f by GOBOARD7:34, XXREAL_0:2; then A12: 1 + 1 in dom f by FINSEQ_3:25; then consider i1, j1 being Element of NAT such that A13: [i1,j1] in Indices (GoB f) and A14: f /. 2 = (GoB f) * (i1,j1) by GOBOARD2:14; A15: 1 <= j1 by A13, MATRIX_1:38; A16: j1 <= width (GoB f) by A13, MATRIX_1:38; A17: 1 <= i1 by A13, MATRIX_1:38; A18: i1 <= len (GoB f) by A13, MATRIX_1:38; now__::_thesis:_not_j1_<_width_(GoB_f) A19: (f /. 2) `2 = (N-min (L~ f)) `2 by A10, PSCOMP_1:39 .= N-bound (L~ f) by EUCLID:52 ; assume A20: j1 < width (GoB f) ; ::_thesis: contradiction ((GoB f) * (i1,(width (GoB f)))) `2 = ((GoB f) * (1,(width (GoB f)))) `2 by A9, A17, A18, GOBOARD5:1 .= N-bound (L~ f) by JORDAN5D:40 ; hence contradiction by A14, A15, A17, A18, A20, A19, GOBOARD5:4; ::_thesis: verum end; then A21: j1 = width (GoB f) by A16, XXREAL_0:1; A22: now__::_thesis:_not_i_>_i1 assume i > i1 ; ::_thesis: contradiction then (f /. 2) `1 < (N-min (L~ f)) `1 by A2, A3, A14, A4, A15, A17, A21, GOBOARD5:3; hence contradiction by A10, PSCOMP_1:39; ::_thesis: verum end; A23: 1 <= i by A1, FINSEQ_3:25; then A24: [i,(width (GoB f))] in Indices (GoB f) by A9, A4, MATRIX_1:36; (abs (i - i1)) + 0 = (abs (i - i1)) + (abs ((width (GoB f)) - (width (GoB f)))) by ABSVALUE:2 .= 1 by A2, A12, A13, A14, A8, A24, A21, GOBOARD5:12 ; hence A25: f /. 2 = (GoB f) * ((i + 1),(width (GoB f))) by A14, A21, A22, SEQM_3:41; ::_thesis: f /. ((len f) -' 1) = (GoB f) * (i,((width (GoB f)) -' 1)) A26: (len f) -' 1 <= len f by NAT_D:44; 1 <= (len f) -' 1 by A11, NAT_D:49; then A27: (len f) -' 1 in dom f by A26, FINSEQ_3:25; then consider i2, j2 being Element of NAT such that A28: [i2,j2] in Indices (GoB f) and A29: f /. ((len f) -' 1) = (GoB f) * (i2,j2) by GOBOARD2:14; A30: 1 <= i2 by A28, MATRIX_1:38; A31: j2 <= width (GoB f) by A28, MATRIX_1:38; A32: i2 <= len (GoB f) by A28, MATRIX_1:38; len f in dom f by A7, FINSEQ_3:25; then A33: (abs (i2 - i)) + (abs (j2 - (width (GoB f)))) = 1 by A2, A24, A6, A5, A27, A28, A29, GOBOARD5:12; percases ( ( abs (i2 - i) = 1 & j2 = width (GoB f) ) or ( abs (j2 - (width (GoB f))) = 1 & i2 = i ) ) by A33, SEQM_3:42; supposethat A34: abs (i2 - i) = 1 and A35: j2 = width (GoB f) ; ::_thesis: f /. ((len f) -' 1) = (GoB f) * (i,((width (GoB f)) -' 1)) (f /. ((len f) -' 1)) `2 = ((GoB f) * (1,(width (GoB f)))) `2 by A9, A29, A30, A32, A35, GOBOARD5:1 .= (N-min (L~ f)) `2 by A2, A3, A9, A23, A4, GOBOARD5:1 .= N-bound (L~ f) by EUCLID:52 ; then A36: f /. ((len f) -' 1) in N-most (L~ f) by A11, A27, GOBOARD1:1, SPRECT_2:10; now__::_thesis:_contradiction percases ( i > i2 or i + 1 = i2 ) by A34, SEQM_3:41; suppose i > i2 ; ::_thesis: contradiction then (f /. ((len f) -' 1)) `1 < (N-min (L~ f)) `1 by A2, A3, A9, A4, A29, A30, A35, GOBOARD5:3; hence contradiction by A36, PSCOMP_1:39; ::_thesis: verum end; suppose i + 1 = i2 ; ::_thesis: contradiction then 2 >= (len f) -' 1 by A25, A26, A29, A35, GOBOARD7:37; then 2 + 1 >= len f by NAT_D:52; hence contradiction by GOBOARD7:34, XXREAL_0:2; ::_thesis: verum end; end; end; hence f /. ((len f) -' 1) = (GoB f) * (i,((width (GoB f)) -' 1)) ; ::_thesis: verum end; supposethat A37: abs (j2 - (width (GoB f))) = 1 and A38: i2 = i ; ::_thesis: f /. ((len f) -' 1) = (GoB f) * (i,((width (GoB f)) -' 1)) width (GoB f) in NAT ; then width (GoB f) = j2 + 1 by A31, A37, SEQM_3:41; hence f /. ((len f) -' 1) = (GoB f) * (i,((width (GoB f)) -' 1)) by A29, A38, NAT_D:34; ::_thesis: verum end; end; end; theorem :: SPRECT_3:30 for i, j being Element of NAT for f being non constant standard special_circular_sequence st 1 <= i & i < j & j <= len f & f /. 1 in L~ (mid (f,i,j)) & not i = 1 holds j = len f proof let i, j be Element of NAT ; ::_thesis: for f being non constant standard special_circular_sequence st 1 <= i & i < j & j <= len f & f /. 1 in L~ (mid (f,i,j)) & not i = 1 holds j = len f let f be non constant standard special_circular_sequence; ::_thesis: ( 1 <= i & i < j & j <= len f & f /. 1 in L~ (mid (f,i,j)) & not i = 1 implies j = len f ) assume that A1: 1 <= i and A2: i < j and A3: j <= len f ; ::_thesis: ( not f /. 1 in L~ (mid (f,i,j)) or i = 1 or j = len f ) 1 + 1 <= len f by GOBOARD7:34, XXREAL_0:2; then A4: f /. 1 in LSeg (f,1) by TOPREAL1:21; assume f /. 1 in L~ (mid (f,i,j)) ; ::_thesis: ( i = 1 or j = len f ) then consider n being Element of NAT such that A5: 1 <= n and A6: n + 1 <= len (mid (f,i,j)) and A7: f /. 1 in LSeg ((mid (f,i,j)),n) by SPPOL_2:13; n < len (mid (f,i,j)) by A6, NAT_1:13; then A8: n < (j -' i) + 1 by A1, A2, A3, JORDAN4:8; then LSeg ((mid (f,i,j)),n) = LSeg (f,((n + i) -' 1)) by A1, A2, A3, A5, JORDAN4:19; then A9: f /. 1 in (LSeg (f,1)) /\ (LSeg (f,((n + i) -' 1))) by A7, A4, XBOOLE_0:def_4; then A10: LSeg (f,1) meets LSeg (f,((n + i) -' 1)) by XBOOLE_0:4; assume that A11: i <> 1 and A12: j <> len f ; ::_thesis: contradiction percases ( 1 + 1 >= (n + i) -' 1 or ((n + i) -' 1) + 1 >= len f ) by A10, GOBOARD5:def_4; suppose 1 + 1 >= (n + i) -' 1 ; ::_thesis: contradiction then A13: n + i <= 2 + 1 by NAT_D:52; i > 1 by A1, A11, XXREAL_0:1; then A14: i >= 1 + 1 by NAT_1:13; n + i >= i + 1 by A5, XREAL_1:6; then i + 1 <= 2 + 1 by A13, XXREAL_0:2; then i <= 2 by XREAL_1:6; then A15: i = 2 by A14, XXREAL_0:1; then n <= 1 by A13, XREAL_1:6; then n = 1 by A5, XXREAL_0:1; then A16: (n + i) -' 1 = 2 by A15, NAT_D:34; A17: 2 < len f by GOBOARD7:34, XXREAL_0:2; 1 + 2 <= len f by GOBOARD7:34, XXREAL_0:2; then (LSeg (f,1)) /\ (LSeg (f,(1 + 1))) = {(f /. (1 + 1))} by TOPREAL1:def_6; then f /. 1 = f /. 2 by A9, A16, TARSKI:def_1; hence contradiction by A17, GOBOARD7:36; ::_thesis: verum end; supposeA18: ((n + i) -' 1) + 1 >= len f ; ::_thesis: contradiction n <= n + i by NAT_1:11; then A19: len f <= n + i by A5, A18, XREAL_1:235, XXREAL_0:2; ((j -' i) + 1) + i = ((j -' i) + i) + 1 .= j + 1 by A2, XREAL_1:235 ; then n + i < j + 1 by A8, XREAL_1:6; then A20: n + i <= j by NAT_1:13; j < len f by A3, A12, XXREAL_0:1; hence contradiction by A19, A20, XXREAL_0:2; ::_thesis: verum end; end; end; theorem :: SPRECT_3:31 for f being non constant standard clockwise_oriented special_circular_sequence st f /. 1 = N-min (L~ f) holds LSeg ((f /. 1),(f /. 2)) c= L~ (SpStSeq (L~ f)) proof let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( f /. 1 = N-min (L~ f) implies LSeg ((f /. 1),(f /. 2)) c= L~ (SpStSeq (L~ f)) ) A1: N-most (L~ f) c= LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by XBOOLE_1:17; assume A2: f /. 1 = N-min (L~ f) ; ::_thesis: LSeg ((f /. 1),(f /. 2)) c= L~ (SpStSeq (L~ f)) then A3: f /. 2 in N-most (L~ f) by SPRECT_2:30; A4: LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) c= L~ (SpStSeq (L~ f)) by Th14; f /. 1 in LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by A2, Th15; then LSeg ((f /. 1),(f /. 2)) c= LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by A3, A1, TOPREAL1:6; hence LSeg ((f /. 1),(f /. 2)) c= L~ (SpStSeq (L~ f)) by A4, XBOOLE_1:1; ::_thesis: verum end; begin theorem Th32: :: SPRECT_3:32 for f being rectangular FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) holds ( not p in L~ f or p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) ) proof let f be rectangular FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) holds ( not p in L~ f or p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) ) let p be Point of (TOP-REAL 2); ::_thesis: ( not p in L~ f or p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) ) assume A1: p in L~ f ; ::_thesis: ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) ) consider D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) such that A2: f = SpStSeq D by SPRECT_1:def_2; L~ f = ((LSeg ((NW-corner D),(NE-corner D))) \/ (LSeg ((NE-corner D),(SE-corner D)))) \/ ((LSeg ((SE-corner D),(SW-corner D))) \/ (LSeg ((SW-corner D),(NW-corner D)))) by A2, SPRECT_1:41; then A3: ( p in (LSeg ((NW-corner D),(NE-corner D))) \/ (LSeg ((NE-corner D),(SE-corner D))) or p in (LSeg ((SE-corner D),(SW-corner D))) \/ (LSeg ((SW-corner D),(NW-corner D))) ) by A1, XBOOLE_0:def_3; percases ( p in LSeg ((NW-corner D),(NE-corner D)) or p in LSeg ((NE-corner D),(SE-corner D)) or p in LSeg ((SE-corner D),(SW-corner D)) or p in LSeg ((SW-corner D),(NW-corner D)) ) by A3, XBOOLE_0:def_3; supposeA4: p in LSeg ((NW-corner D),(NE-corner D)) ; ::_thesis: ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) ) A5: N-bound (L~ (SpStSeq D)) = N-bound D by SPRECT_1:60; then A6: (NE-corner D) `2 = N-bound (L~ f) by A2, EUCLID:52; (NW-corner D) `2 = N-bound (L~ f) by A2, A5, EUCLID:52; hence ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) ) by A4, A6, GOBOARD7:6; ::_thesis: verum end; supposeA7: p in LSeg ((NE-corner D),(SE-corner D)) ; ::_thesis: ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) ) A8: E-bound (L~ (SpStSeq D)) = E-bound D by SPRECT_1:61; then A9: (SE-corner D) `1 = E-bound (L~ f) by A2, EUCLID:52; (NE-corner D) `1 = E-bound (L~ f) by A2, A8, EUCLID:52; hence ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) ) by A7, A9, GOBOARD7:5; ::_thesis: verum end; supposeA10: p in LSeg ((SE-corner D),(SW-corner D)) ; ::_thesis: ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) ) A11: S-bound (L~ (SpStSeq D)) = S-bound D by SPRECT_1:59; then A12: (SW-corner D) `2 = S-bound (L~ f) by A2, EUCLID:52; (SE-corner D) `2 = S-bound (L~ f) by A2, A11, EUCLID:52; hence ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) ) by A10, A12, GOBOARD7:6; ::_thesis: verum end; supposeA13: p in LSeg ((SW-corner D),(NW-corner D)) ; ::_thesis: ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) ) A14: W-bound (L~ (SpStSeq D)) = W-bound D by SPRECT_1:58; then A15: (NW-corner D) `1 = W-bound (L~ f) by A2, EUCLID:52; (SW-corner D) `1 = W-bound (L~ f) by A2, A14, EUCLID:52; hence ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) ) by A13, A15, GOBOARD7:5; ::_thesis: verum end; end; end; registration cluster non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like V236( the U1 of (TOP-REAL 2)) special unfolded s.c.c. rectangular for FinSequence of the U1 of (TOP-REAL 2); existence ex b1 being special_circular_sequence st b1 is rectangular proof set C = the non empty compact non horizontal non vertical Subset of (TOP-REAL 2); SpStSeq the non empty compact non horizontal non vertical Subset of (TOP-REAL 2) is special_circular_sequence ; hence ex b1 being special_circular_sequence st b1 is rectangular ; ::_thesis: verum end; end; theorem Th33: :: SPRECT_3:33 for f being rectangular special_circular_sequence for g being S-Sequence_in_R2 st g /. 1 in LeftComp f & g /. (len g) in RightComp f holds L~ f meets L~ g proof let f be rectangular special_circular_sequence; ::_thesis: for g being S-Sequence_in_R2 st g /. 1 in LeftComp f & g /. (len g) in RightComp f holds L~ f meets L~ g let g be S-Sequence_in_R2; ::_thesis: ( g /. 1 in LeftComp f & g /. (len g) in RightComp f implies L~ f meets L~ g ) assume that A1: g /. 1 in LeftComp f and A2: g /. (len g) in RightComp f ; ::_thesis: L~ f meets L~ g A3: len g >= 2 by TOPREAL1:def_8; then g /. 1 in L~ g by JORDAN3:1; then g /. 1 in (LeftComp f) /\ (L~ g) by A1, XBOOLE_0:def_4; then A4: LeftComp f meets L~ g by XBOOLE_0:4; g /. (len g) in L~ g by A3, JORDAN3:1; then g /. (len g) in (RightComp f) /\ (L~ g) by A2, XBOOLE_0:def_4; then A5: RightComp f meets L~ g by XBOOLE_0:4; A6: LeftComp f misses RightComp f by SPRECT_1:88; assume L~ f misses L~ g ; ::_thesis: contradiction then L~ g c= (L~ f) ` by SUBSET_1:23; then A7: L~ g c= (LeftComp f) \/ (RightComp f) by GOBRD12:10; A8: L~ g is_an_arc_of g /. 1,g /. (len g) by TOPREAL1:25; A9: RightComp f is open by Th24; LeftComp f is open by Th24; hence contradiction by A7, A9, A4, A5, A6, A8, JORDAN6:10, TOPREAL5:1; ::_thesis: verum end; theorem Th34: :: SPRECT_3:34 for f being rectangular special_circular_sequence holds SpStSeq (L~ f) = f proof let f be rectangular special_circular_sequence; ::_thesis: SpStSeq (L~ f) = f set C = L~ f; set g = SpStSeq (L~ f); consider D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) such that A1: f = SpStSeq D by SPRECT_1:def_2; A2: 5 = len f by SPRECT_1:82; SpStSeq (L~ f) = <*(NW-corner (L~ f)),(NE-corner (L~ f)),(SE-corner (L~ f))*> ^ <*(SW-corner (L~ f)),(NW-corner (L~ f))*> by SPRECT_1:def_1; then A3: len (SpStSeq (L~ f)) = (len <*(NW-corner (L~ f)),(NE-corner (L~ f)),(SE-corner (L~ f))*>) + (len <*(SW-corner (L~ f)),(NW-corner (L~ f))*>) by FINSEQ_1:22 .= 3 + (len <*(SW-corner (L~ f)),(NW-corner (L~ f))*>) by FINSEQ_1:45 .= 3 + 2 by FINSEQ_1:44 ; A4: for i being Nat st i in dom f holds f /. i = (SpStSeq (L~ f)) /. i proof let i be Nat; ::_thesis: ( i in dom f implies f /. i = (SpStSeq (L~ f)) /. i ) assume A5: i in dom f ; ::_thesis: f /. i = (SpStSeq (L~ f)) /. i then A6: 0 <> i by FINSEQ_3:25; A7: i <= len f by A5, FINSEQ_3:25; A8: f /. 1 = W-max (L~ f) by SPRECT_1:83 .= NW-corner D by A1, SPRECT_1:75 .= NW-corner (L~ f) by A1, SPRECT_1:62 .= (SpStSeq (L~ f)) /. 1 by SPRECT_1:35 ; percases ( i = 1 or i = 2 or i = 3 or i = 4 or i = 5 ) by A2, A6, A7, NAT_1:29; suppose i = 1 ; ::_thesis: f /. i = (SpStSeq (L~ f)) /. i hence f /. i = (SpStSeq (L~ f)) /. i by A8; ::_thesis: verum end; supposeA9: i = 2 ; ::_thesis: f /. i = (SpStSeq (L~ f)) /. i hence f /. i = E-max (L~ f) by SPRECT_1:84 .= NE-corner D by A1, SPRECT_1:79 .= NE-corner (L~ f) by A1, SPRECT_1:63 .= (SpStSeq (L~ f)) /. i by A9, SPRECT_1:36 ; ::_thesis: verum end; supposeA10: i = 3 ; ::_thesis: f /. i = (SpStSeq (L~ f)) /. i hence f /. i = E-min (L~ f) by SPRECT_1:85 .= SE-corner D by A1, SPRECT_1:78 .= SE-corner (L~ f) by A1, SPRECT_1:65 .= (SpStSeq (L~ f)) /. i by A10, SPRECT_1:37 ; ::_thesis: verum end; supposeA11: i = 4 ; ::_thesis: f /. i = (SpStSeq (L~ f)) /. i hence f /. i = W-min (L~ f) by SPRECT_1:86 .= SW-corner D by A1, SPRECT_1:74 .= SW-corner (L~ f) by A1, SPRECT_1:64 .= (SpStSeq (L~ f)) /. i by A11, SPRECT_1:38 ; ::_thesis: verum end; supposeA12: i = 5 ; ::_thesis: f /. i = (SpStSeq (L~ f)) /. i hence f /. i = f /. 1 by A2, FINSEQ_6:def_1 .= (SpStSeq (L~ f)) /. i by A3, A8, A12, FINSEQ_6:def_1 ; ::_thesis: verum end; end; end; dom f = dom (SpStSeq (L~ f)) by A2, A3, FINSEQ_3:29; hence SpStSeq (L~ f) = f by A4, FINSEQ_5:12; ::_thesis: verum end; theorem Th35: :: SPRECT_3:35 for f being rectangular special_circular_sequence holds L~ f = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) or ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) ) } proof let f be rectangular special_circular_sequence; ::_thesis: L~ f = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) or ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) ) } set C = L~ f; set E = { p where p is Point of (TOP-REAL 2) : ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) } ; set S = { p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) } ; set N = { p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) } ; set W = { p where p is Point of (TOP-REAL 2) : ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) } ; A1: LSeg ((SE-corner (L~ f)),(NE-corner (L~ f))) = { p where p is Point of (TOP-REAL 2) : ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) } by SPRECT_1:23; A2: LSeg ((SW-corner (L~ f)),(SE-corner (L~ f))) = { p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) } by SPRECT_1:24; A3: LSeg ((SW-corner (L~ f)),(NW-corner (L~ f))) = { p where p is Point of (TOP-REAL 2) : ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) } by SPRECT_1:26; A4: LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) = { p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) } by SPRECT_1:25; A5: L~ f = L~ (SpStSeq (L~ f)) by Th34; thus L~ f c= { p where p is Point of (TOP-REAL 2) : ( ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) or ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) ) } :: according to XBOOLE_0:def_10 ::_thesis: { p where p is Point of (TOP-REAL 2) : ( ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) or ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) ) } c= L~ f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L~ f or x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) or ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) ) } ) assume A6: x in L~ f ; ::_thesis: x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) or ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) ) } then reconsider q = x as Point of (TOP-REAL 2) ; q in ((LSeg ((NW-corner (L~ f)),(NE-corner (L~ f)))) \/ (LSeg ((NE-corner (L~ f)),(SE-corner (L~ f))))) \/ ((LSeg ((SE-corner (L~ f)),(SW-corner (L~ f)))) \/ (LSeg ((SW-corner (L~ f)),(NW-corner (L~ f))))) by A5, A6, SPRECT_1:41; then ( q in (LSeg ((NW-corner (L~ f)),(NE-corner (L~ f)))) \/ (LSeg ((NE-corner (L~ f)),(SE-corner (L~ f)))) or q in (LSeg ((SE-corner (L~ f)),(SW-corner (L~ f)))) \/ (LSeg ((SW-corner (L~ f)),(NW-corner (L~ f)))) ) by XBOOLE_0:def_3; then ( q in LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) or q in LSeg ((NE-corner (L~ f)),(SE-corner (L~ f))) or q in LSeg ((SE-corner (L~ f)),(SW-corner (L~ f))) or q in LSeg ((SW-corner (L~ f)),(NW-corner (L~ f))) ) by XBOOLE_0:def_3; then ( ex p being Point of (TOP-REAL 2) st ( x = p & p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) or ex p being Point of (TOP-REAL 2) st ( x = p & p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) or ex p being Point of (TOP-REAL 2) st ( x = p & p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) or ex p being Point of (TOP-REAL 2) st ( x = p & p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) ) by A1, A2, A4, A3; hence x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) or ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) ) } ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) or ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) ) } or x in L~ f ) assume x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) or ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) ) } ; ::_thesis: x in L~ f then ex p being Point of (TOP-REAL 2) st ( x = p & ( ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) or ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) ) ) ; then ( x in LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) or x in LSeg ((NE-corner (L~ f)),(SE-corner (L~ f))) or x in LSeg ((SE-corner (L~ f)),(SW-corner (L~ f))) or x in LSeg ((SW-corner (L~ f)),(NW-corner (L~ f))) ) by A1, A2, A4, A3; then ( x in (LSeg ((NW-corner (L~ f)),(NE-corner (L~ f)))) \/ (LSeg ((NE-corner (L~ f)),(SE-corner (L~ f)))) or x in (LSeg ((SE-corner (L~ f)),(SW-corner (L~ f)))) \/ (LSeg ((SW-corner (L~ f)),(NW-corner (L~ f)))) ) by XBOOLE_0:def_3; then x in ((LSeg ((NW-corner (L~ f)),(NE-corner (L~ f)))) \/ (LSeg ((NE-corner (L~ f)),(SE-corner (L~ f))))) \/ ((LSeg ((SE-corner (L~ f)),(SW-corner (L~ f)))) \/ (LSeg ((SW-corner (L~ f)),(NW-corner (L~ f))))) by XBOOLE_0:def_3; hence x in L~ f by A5, SPRECT_1:41; ::_thesis: verum end; theorem Th36: :: SPRECT_3:36 for f being rectangular special_circular_sequence holds GoB f = ((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2)) proof let f be rectangular special_circular_sequence; ::_thesis: GoB f = ((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2)) set G = ((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2)); set v1 = Incr (X_axis f); set v2 = Incr (Y_axis f); A1: f /. 2 = N-max (L~ f) by SPRECT_1:84; A2: f /. 1 = N-min (L~ f) by SPRECT_1:83; then A3: (f /. 1) `1 < (f /. 2) `1 by A1, SPRECT_2:51; A4: (f /. 2) `2 = (f /. 1) `2 by A2, A1, PSCOMP_1:37; A5: f /. 4 = S-min (L~ f) by SPRECT_1:86; A6: f /. 3 = S-max (L~ f) by SPRECT_1:85; then A7: (f /. 3) `2 = (f /. 4) `2 by A5, PSCOMP_1:53; A8: len <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*> = 3 by FINSEQ_1:45; A9: len f = 5 by SPRECT_1:82; then A10: f /. 1 = f /. 5 by FINSEQ_6:def_1; set g = <*((f /. 1) `1),((f /. 2) `1)*>; set h = <*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>; A11: f /. 3 = E-min (L~ f) by SPRECT_1:85; A12: f /. 2 = E-max (L~ f) by SPRECT_1:84; then A13: (f /. 3) `1 = (f /. 2) `1 by A11, PSCOMP_1:45; A14: len <*((f /. 1) `1),((f /. 2) `1)*> = 2 by FINSEQ_1:44; A15: dom <*((f /. 1) `1),((f /. 2) `1)*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89; A16: <*((f /. 1) `1),((f /. 2) `1)*> is increasing proof A17: <*((f /. 1) `1),((f /. 2) `1)*> . 2 = (f /. 2) `1 by FINSEQ_1:44; A18: <*((f /. 1) `1),((f /. 2) `1)*> . 1 = (f /. 1) `1 by FINSEQ_1:44; let n be Element of NAT ; :: according to SEQM_3:def_1 ::_thesis: for b1 being Element of NAT holds ( not n in K74(<*((f /. 1) `1),((f /. 2) `1)*>) or not b1 in K74(<*((f /. 1) `1),((f /. 2) `1)*>) or b1 <= n or not K571(<*((f /. 1) `1),((f /. 2) `1)*>,b1) <= K571(<*((f /. 1) `1),((f /. 2) `1)*>,n) ) let m be Element of NAT ; ::_thesis: ( not n in K74(<*((f /. 1) `1),((f /. 2) `1)*>) or not m in K74(<*((f /. 1) `1),((f /. 2) `1)*>) or m <= n or not K571(<*((f /. 1) `1),((f /. 2) `1)*>,m) <= K571(<*((f /. 1) `1),((f /. 2) `1)*>,n) ) assume that A19: n in dom <*((f /. 1) `1),((f /. 2) `1)*> and A20: m in dom <*((f /. 1) `1),((f /. 2) `1)*> and A21: n < m ; ::_thesis: not K571(<*((f /. 1) `1),((f /. 2) `1)*>,m) <= K571(<*((f /. 1) `1),((f /. 2) `1)*>,n) A22: ( m = 1 or m = 2 ) by A15, A20, TARSKI:def_2; ( n = 1 or n = 2 ) by A15, A19, TARSKI:def_2; hence <*((f /. 1) `1),((f /. 2) `1)*> . n < <*((f /. 1) `1),((f /. 2) `1)*> . m by A2, A1, A21, A18, A17, A22, SPRECT_2:51; ::_thesis: verum end; A23: f /. 4 = W-min (L~ f) by SPRECT_1:86; A24: len (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) = (len <*((f /. 1) `1),((f /. 2) `1)*>) + (len <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) by FINSEQ_1:22 .= (len <*((f /. 1) `1),((f /. 2) `1)*>) + 3 by FINSEQ_1:45 .= 2 + 3 by FINSEQ_1:44 .= len f by SPRECT_1:82 ; for n being Element of NAT st n in dom (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) holds (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) . n = (f /. n) `1 proof let n be Element of NAT ; ::_thesis: ( n in dom (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) implies (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) . n = (f /. n) `1 ) assume A25: n in dom (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) ; ::_thesis: (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) . n = (f /. n) `1 then A26: 1 <= n by FINSEQ_3:25; A27: n <= 5 by A9, A24, A25, FINSEQ_3:25; percases ( n = 1 or n = 2 or n = 3 or n = 4 or n = 5 ) by A26, A27, NAT_1:29; supposeA28: n = 1 ; ::_thesis: (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) . n = (f /. n) `1 then n in dom <*((f /. 1) `1),((f /. 2) `1)*> by A14, FINSEQ_3:25; hence (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) . n = <*((f /. 1) `1),((f /. 2) `1)*> . 1 by A28, FINSEQ_1:def_7 .= (f /. n) `1 by A28, FINSEQ_1:44 ; ::_thesis: verum end; supposeA29: n = 2 ; ::_thesis: (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) . n = (f /. n) `1 then n in dom <*((f /. 1) `1),((f /. 2) `1)*> by A14, FINSEQ_3:25; hence (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) . n = <*((f /. 1) `1),((f /. 2) `1)*> . 2 by A29, FINSEQ_1:def_7 .= (f /. n) `1 by A29, FINSEQ_1:44 ; ::_thesis: verum end; supposeA30: n = 3 ; ::_thesis: (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) . n = (f /. n) `1 hence (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) . n = (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) . (2 + 1) .= <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*> . 1 by A14, A8, FINSEQ_1:65 .= (f /. n) `1 by A30, FINSEQ_1:45 ; ::_thesis: verum end; supposeA31: n = 4 ; ::_thesis: (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) . n = (f /. n) `1 hence (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) . n = (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) . (2 + 2) .= <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*> . 2 by A14, A8, FINSEQ_1:65 .= (f /. n) `1 by A31, FINSEQ_1:45 ; ::_thesis: verum end; supposeA32: n = 5 ; ::_thesis: (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) . n = (f /. n) `1 hence (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) . n = (<*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) . (2 + 3) .= <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*> . 3 by A14, A8, FINSEQ_1:65 .= (f /. n) `1 by A32, FINSEQ_1:45 ; ::_thesis: verum end; end; end; then A33: X_axis f = <*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*> by A24, GOBOARD1:def_1; A34: rng <*((f /. 1) `1),((f /. 2) `1)*> = {((f /. 1) `1),((f /. 2) `1)} by FINSEQ_2:127; A35: f /. 1 = W-max (L~ f) by SPRECT_1:83; then A36: (f /. 4) `2 < (f /. 5) `2 by A23, A10, SPRECT_2:57; {((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)} c= {((f /. 1) `1),((f /. 2) `1)} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)} or x in {((f /. 1) `1),((f /. 2) `1)} ) assume A37: x in {((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)} ; ::_thesis: x in {((f /. 1) `1),((f /. 2) `1)} percases ( x = (f /. 3) `1 or x = (f /. 4) `1 or x = (f /. 5) `1 ) by A37, ENUMSET1:def_1; suppose x = (f /. 3) `1 ; ::_thesis: x in {((f /. 1) `1),((f /. 2) `1)} then x = (f /. 2) `1 by A12, A11, PSCOMP_1:45; hence x in {((f /. 1) `1),((f /. 2) `1)} by TARSKI:def_2; ::_thesis: verum end; suppose x = (f /. 4) `1 ; ::_thesis: x in {((f /. 1) `1),((f /. 2) `1)} then x = (f /. 1) `1 by A35, A23, PSCOMP_1:29; hence x in {((f /. 1) `1),((f /. 2) `1)} by TARSKI:def_2; ::_thesis: verum end; suppose x = (f /. 5) `1 ; ::_thesis: x in {((f /. 1) `1),((f /. 2) `1)} then x = (f /. 1) `1 by A9, FINSEQ_6:def_1; hence x in {((f /. 1) `1),((f /. 2) `1)} by TARSKI:def_2; ::_thesis: verum end; end; end; then A38: rng <*((f /. 1) `1),((f /. 2) `1)*> = (rng <*((f /. 1) `1),((f /. 2) `1)*>) \/ {((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)} by A34, XBOOLE_1:12 .= (rng <*((f /. 1) `1),((f /. 2) `1)*>) \/ (rng <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) by FINSEQ_2:128 .= rng (X_axis f) by A33, FINSEQ_1:31 ; len <*((f /. 1) `1),((f /. 2) `1)*> = 2 by FINSEQ_1:44 .= card (rng (X_axis f)) by A34, A38, A3, CARD_2:57 ; then A39: Incr (X_axis f) = <*((f /. 1) `1),((f /. 2) `1)*> by A38, A16, SEQ_4:def_21; then A40: (Incr (X_axis f)) . 1 = (f /. 1) `1 by FINSEQ_1:44; set g = <*((f /. 4) `2),((f /. 5) `2)*>; set h = <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>; A41: len (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) = (len <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*>) + (len <*((f /. 4) `2),((f /. 5) `2)*>) by FINSEQ_1:22 .= (len <*((f /. 4) `2),((f /. 5) `2)*>) + 3 by FINSEQ_1:45 .= 2 + 3 by FINSEQ_1:44 .= len f by SPRECT_1:82 ; A42: len <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> = 3 by FINSEQ_1:45; A43: dom <*((f /. 4) `2),((f /. 5) `2)*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89; A44: <*((f /. 4) `2),((f /. 5) `2)*> is increasing proof A45: <*((f /. 4) `2),((f /. 5) `2)*> . 2 = (f /. 5) `2 by FINSEQ_1:44; A46: <*((f /. 4) `2),((f /. 5) `2)*> . 1 = (f /. 4) `2 by FINSEQ_1:44; let n be Element of NAT ; :: according to SEQM_3:def_1 ::_thesis: for b1 being Element of NAT holds ( not n in K74(<*((f /. 4) `2),((f /. 5) `2)*>) or not b1 in K74(<*((f /. 4) `2),((f /. 5) `2)*>) or b1 <= n or not K571(<*((f /. 4) `2),((f /. 5) `2)*>,b1) <= K571(<*((f /. 4) `2),((f /. 5) `2)*>,n) ) let m be Element of NAT ; ::_thesis: ( not n in K74(<*((f /. 4) `2),((f /. 5) `2)*>) or not m in K74(<*((f /. 4) `2),((f /. 5) `2)*>) or m <= n or not K571(<*((f /. 4) `2),((f /. 5) `2)*>,m) <= K571(<*((f /. 4) `2),((f /. 5) `2)*>,n) ) assume that A47: n in dom <*((f /. 4) `2),((f /. 5) `2)*> and A48: m in dom <*((f /. 4) `2),((f /. 5) `2)*> and A49: n < m ; ::_thesis: not K571(<*((f /. 4) `2),((f /. 5) `2)*>,m) <= K571(<*((f /. 4) `2),((f /. 5) `2)*>,n) A50: ( m = 1 or m = 2 ) by A43, A48, TARSKI:def_2; ( n = 1 or n = 2 ) by A43, A47, TARSKI:def_2; hence <*((f /. 4) `2),((f /. 5) `2)*> . n < <*((f /. 4) `2),((f /. 5) `2)*> . m by A35, A23, A10, A49, A46, A45, A50, SPRECT_2:57; ::_thesis: verum end; A51: (Incr (X_axis f)) . 2 = (f /. 2) `1 by A39, FINSEQ_1:44; A52: len <*((f /. 4) `2),((f /. 5) `2)*> = 2 by FINSEQ_1:44; for n being Element of NAT st n in dom (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) holds (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) . n = (f /. n) `2 proof let n be Element of NAT ; ::_thesis: ( n in dom (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) implies (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) . n = (f /. n) `2 ) assume A53: n in dom (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) ; ::_thesis: (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) . n = (f /. n) `2 then A54: 1 <= n by FINSEQ_3:25; A55: n <= 5 by A9, A41, A53, FINSEQ_3:25; percases ( n = 1 or n = 2 or n = 3 or n = 4 or n = 5 ) by A54, A55, NAT_1:29; supposeA56: n = 1 ; ::_thesis: (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) . n = (f /. n) `2 then n in dom <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> by A42, FINSEQ_3:25; hence (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) . n = <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> . 1 by A56, FINSEQ_1:def_7 .= (f /. n) `2 by A56, FINSEQ_1:45 ; ::_thesis: verum end; supposeA57: n = 2 ; ::_thesis: (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) . n = (f /. n) `2 then n in dom <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> by A42, FINSEQ_3:25; hence (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) . n = <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> . 2 by A57, FINSEQ_1:def_7 .= (f /. n) `2 by A57, FINSEQ_1:45 ; ::_thesis: verum end; supposeA58: n = 3 ; ::_thesis: (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) . n = (f /. n) `2 then n in dom <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> by A42, FINSEQ_3:25; hence (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) . n = <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> . 3 by A58, FINSEQ_1:def_7 .= (f /. n) `2 by A58, FINSEQ_1:45 ; ::_thesis: verum end; supposeA59: n = 4 ; ::_thesis: (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) . n = (f /. n) `2 hence (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) . n = (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) . (3 + 1) .= <*((f /. 4) `2),((f /. 5) `2)*> . 1 by A52, A42, FINSEQ_1:65 .= (f /. n) `2 by A59, FINSEQ_1:44 ; ::_thesis: verum end; supposeA60: n = 5 ; ::_thesis: (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) . n = (f /. n) `2 hence (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) . n = (<*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*>) . (2 + 3) .= <*((f /. 4) `2),((f /. 5) `2)*> . 2 by A52, A42, FINSEQ_1:65 .= (f /. n) `2 by A60, FINSEQ_1:44 ; ::_thesis: verum end; end; end; then A61: Y_axis f = <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*> by A41, GOBOARD1:def_2; A62: rng <*((f /. 4) `2),((f /. 5) `2)*> = {((f /. 4) `2),((f /. 5) `2)} by FINSEQ_2:127; {((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)} c= {((f /. 4) `2),((f /. 5) `2)} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)} or x in {((f /. 4) `2),((f /. 5) `2)} ) assume A63: x in {((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)} ; ::_thesis: x in {((f /. 4) `2),((f /. 5) `2)} percases ( x = (f /. 1) `2 or x = (f /. 2) `2 or x = (f /. 3) `2 ) by A63, ENUMSET1:def_1; suppose x = (f /. 1) `2 ; ::_thesis: x in {((f /. 4) `2),((f /. 5) `2)} hence x in {((f /. 4) `2),((f /. 5) `2)} by A10, TARSKI:def_2; ::_thesis: verum end; suppose x = (f /. 2) `2 ; ::_thesis: x in {((f /. 4) `2),((f /. 5) `2)} then x = (f /. 1) `2 by A2, A1, PSCOMP_1:37; hence x in {((f /. 4) `2),((f /. 5) `2)} by A10, TARSKI:def_2; ::_thesis: verum end; suppose x = (f /. 3) `2 ; ::_thesis: x in {((f /. 4) `2),((f /. 5) `2)} then x = (f /. 4) `2 by A6, A5, PSCOMP_1:53; hence x in {((f /. 4) `2),((f /. 5) `2)} by TARSKI:def_2; ::_thesis: verum end; end; end; then A64: rng <*((f /. 4) `2),((f /. 5) `2)*> = {((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)} \/ {((f /. 4) `2),((f /. 5) `2)} by A62, XBOOLE_1:12 .= (rng <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*>) \/ {((f /. 4) `2),((f /. 5) `2)} by FINSEQ_2:128 .= (rng <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*>) \/ (rng <*((f /. 4) `2),((f /. 5) `2)*>) by FINSEQ_2:127 .= rng (Y_axis f) by A61, FINSEQ_1:31 ; len <*((f /. 4) `2),((f /. 5) `2)*> = 2 by FINSEQ_1:44 .= card (rng (Y_axis f)) by A62, A64, A36, CARD_2:57 ; then A65: Incr (Y_axis f) = <*((f /. 4) `2),((f /. 1) `2)*> by A10, A64, A44, SEQ_4:def_21; then A66: (Incr (Y_axis f)) . 1 = (f /. 4) `2 by FINSEQ_1:44; A67: (Incr (Y_axis f)) . 2 = (f /. 1) `2 by A65, FINSEQ_1:44; A68: (f /. 1) `1 = (f /. 4) `1 by A35, A23, PSCOMP_1:29; A69: for n, m being Element of NAT st [n,m] in Indices (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) holds (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| proof let n, m be Element of NAT ; ::_thesis: ( [n,m] in Indices (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) implies (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| ) assume [n,m] in Indices (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) ; ::_thesis: (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| then A70: [n,m] in {[1,1],[1,2],[2,1],[2,2]} by Th2; percases ( [n,m] = [1,1] or [n,m] = [1,2] or [n,m] = [2,1] or [n,m] = [2,2] ) by A70, ENUMSET1:def_2; supposeA71: [n,m] = [1,1] ; ::_thesis: (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| then A72: m = 1 by XTUPLE_0:1; A73: n = 1 by A71, XTUPLE_0:1; hence (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = f /. 4 by A72, MATRIX_2:6 .= |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A40, A66, A68, A73, A72, EUCLID:53 ; ::_thesis: verum end; supposeA74: [n,m] = [1,2] ; ::_thesis: (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| then A75: m = 2 by XTUPLE_0:1; A76: n = 1 by A74, XTUPLE_0:1; hence (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = f /. 1 by A75, MATRIX_2:6 .= |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A40, A67, A76, A75, EUCLID:53 ; ::_thesis: verum end; supposeA77: [n,m] = [2,1] ; ::_thesis: (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| then A78: m = 1 by XTUPLE_0:1; A79: n = 2 by A77, XTUPLE_0:1; hence (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = f /. 3 by A78, MATRIX_2:6 .= |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A51, A66, A13, A7, A79, A78, EUCLID:53 ; ::_thesis: verum end; supposeA80: [n,m] = [2,2] ; ::_thesis: (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| then A81: m = 2 by XTUPLE_0:1; A82: n = 2 by A80, XTUPLE_0:1; hence (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = f /. 2 by A81, MATRIX_2:6 .= |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A51, A67, A4, A82, A81, EUCLID:53 ; ::_thesis: verum end; end; end; A83: width (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) = 2 by MATRIX_2:3 .= len (Incr (Y_axis f)) by A65, FINSEQ_1:44 ; len (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) = 2 by MATRIX_2:3 .= len (Incr (X_axis f)) by A39, FINSEQ_1:44 ; then GoB ((Incr (X_axis f)),(Incr (Y_axis f))) = ((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2)) by A83, A69, GOBOARD2:def_1; hence GoB f = ((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2)) by GOBOARD2:def_2; ::_thesis: verum end; theorem Th37: :: SPRECT_3:37 for f being rectangular special_circular_sequence holds ( LeftComp f = { p where p is Point of (TOP-REAL 2) : ( not W-bound (L~ f) <= p `1 or not p `1 <= E-bound (L~ f) or not S-bound (L~ f) <= p `2 or not p `2 <= N-bound (L~ f) ) } & RightComp f = { q where q is Point of (TOP-REAL 2) : ( W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) } ) proof let f be rectangular special_circular_sequence; ::_thesis: ( LeftComp f = { p where p is Point of (TOP-REAL 2) : ( not W-bound (L~ f) <= p `1 or not p `1 <= E-bound (L~ f) or not S-bound (L~ f) <= p `2 or not p `2 <= N-bound (L~ f) ) } & RightComp f = { q where q is Point of (TOP-REAL 2) : ( W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) } ) defpred S1[ Element of (TOP-REAL 2)] means ( not W-bound (L~ f) <= $1 `1 or not $1 `1 <= E-bound (L~ f) or not S-bound (L~ f) <= $1 `2 or not $1 `2 <= N-bound (L~ f) ); defpred S2[ Element of (TOP-REAL 2)] means ( W-bound (L~ f) < $1 `1 & $1 `1 < E-bound (L~ f) & S-bound (L~ f) < $1 `2 & $1 `2 < N-bound (L~ f) ); defpred S3[ Element of (TOP-REAL 2)] means ( ( $1 `1 = W-bound (L~ f) & $1 `2 <= N-bound (L~ f) & $1 `2 >= S-bound (L~ f) ) or ( $1 `1 <= E-bound (L~ f) & $1 `1 >= W-bound (L~ f) & $1 `2 = N-bound (L~ f) ) or ( $1 `1 <= E-bound (L~ f) & $1 `1 >= W-bound (L~ f) & $1 `2 = S-bound (L~ f) ) or ( $1 `1 = E-bound (L~ f) & $1 `2 <= N-bound (L~ f) & $1 `2 >= S-bound (L~ f) ) ); set LC = { p where p is Point of (TOP-REAL 2) : S1[p] } ; set RC = { q where q is Point of (TOP-REAL 2) : S2[q] } ; set Lf = { p where p is Point of (TOP-REAL 2) : S3[p] } ; A1: S-bound (L~ f) < N-bound (L~ f) by SPRECT_1:32; A2: { p where p is Point of (TOP-REAL 2) : S3[p] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch_7(); A3: { q where q is Point of (TOP-REAL 2) : S2[q] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch_7(); A4: L~ f = { p where p is Point of (TOP-REAL 2) : S3[p] } by Th35; { p where p is Point of (TOP-REAL 2) : S1[p] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch_7(); then reconsider Lc9 = { p where p is Point of (TOP-REAL 2) : S1[p] } , Rc9 = { q where q is Point of (TOP-REAL 2) : S2[q] } , Lf = { p where p is Point of (TOP-REAL 2) : S3[p] } as Subset of (TOP-REAL 2) by A3, A2; reconsider Lf = Lf as Subset of (TOP-REAL 2) ; reconsider Lc9 = Lc9, Rc9 = Rc9 as Subset of (TOP-REAL 2) ; A5: W-bound (L~ f) < E-bound (L~ f) by SPRECT_1:31; then reconsider Lc = Lc9, Rc = Rc9 as Subset of ((TOP-REAL 2) | (Lf `)) by A1, JORDAN1:39, JORDAN1:41; reconsider Lc = Lc, Rc = Rc as Subset of ((TOP-REAL 2) | (Lf `)) ; A6: ((1 / 2) * (S-bound (L~ f))) + ((1 / 2) * (S-bound (L~ f))) = S-bound (L~ f) ; Rc = Rc9 ; then Lc is a_component by A5, A1, JORDAN1:36; then A7: Lc9 is_a_component_of Lf ` by CONNSP_1:def_6; set p = ((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) + |[0,1]|; set q = (1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f))))); A8: 1 + 1 <= len f by GOBOARD7:34, XXREAL_0:2; A9: (((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) + |[0,1]|) `2 = (((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) `2) + (|[0,1]| `2) by TOPREAL3:2 .= (((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) `2) + 1 by EUCLID:52 ; A10: GoB f = ((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2)) by Th36; then A11: 1 + 1 = width (GoB f) by MATRIX_2:3; then ((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) `2 = ((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + (f /. 2))) `2 by A10, MATRIX_2:6 .= ((1 / 2) * ((f /. 1) + (f /. 2))) `2 by A10, A11, MATRIX_2:6 .= (1 / 2) * (((f /. 1) + (f /. 2)) `2) by TOPREAL3:4 .= (1 / 2) * (((f /. 1) `2) + ((f /. 2) `2)) by TOPREAL3:2 .= (1 / 2) * (((N-min (L~ f)) `2) + ((f /. 2) `2)) by SPRECT_1:83 .= (1 / 2) * (((N-min (L~ f)) `2) + ((N-max (L~ f)) `2)) by SPRECT_1:84 .= (1 / 2) * ((N-bound (L~ f)) + ((N-max (L~ f)) `2)) by EUCLID:52 .= (1 / 2) * ((N-bound (L~ f)) + (N-bound (L~ f))) by EUCLID:52 .= N-bound (L~ f) ; then (((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) + |[0,1]|) `2 > 0 + (N-bound (L~ f)) by A9, XREAL_1:8; then A12: ((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) + |[0,1]| in { p where p is Point of (TOP-REAL 2) : S1[p] } ; A13: 1 + 1 = len (GoB f) by A10, MATRIX_2:3; then A14: ((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * ((1 + 1),(width (GoB f)))))) + |[0,1]| in Int (cell ((GoB f),1,(1 + 1))) by A11, GOBOARD6:32; A15: f /. (1 + 1) = (GoB f) * ((1 + 1),(1 + 1)) by A10, MATRIX_2:6; 1 < width (GoB f) by GOBOARD7:33; then A16: 1 + 1 <= width (GoB f) by NAT_1:13; then A17: [(1 + 1),(1 + 1)] in Indices (GoB f) by A13, MATRIX_1:36; 1 <= len (GoB f) by GOBOARD7:32; then A18: [1,(1 + 1)] in Indices (GoB f) by A16, MATRIX_1:36; A19: f /. 1 = (GoB f) * (1,(1 + 1)) by A10, MATRIX_2:6; then right_cell (f,1) = cell ((GoB f),1,1) by A8, A18, A17, A15, GOBOARD5:28; then A20: Int (cell ((GoB f),1,1)) c= RightComp f by GOBOARD9:def_2; left_cell (f,1) = cell ((GoB f),1,(1 + 1)) by A8, A18, A19, A17, A15, GOBOARD5:28; then Int (cell ((GoB f),1,(1 + 1))) c= LeftComp f by GOBOARD9:def_1; then A21: { p where p is Point of (TOP-REAL 2) : S1[p] } meets LeftComp f by A14, A12, XBOOLE_0:3; A22: (f /. 2) `1 = (E-max (L~ f)) `1 by SPRECT_1:84 .= E-bound (L~ f) by EUCLID:52 ; set p = (1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2))); A23: (1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2))) in Int (cell ((GoB f),1,1)) by A13, A11, GOBOARD6:31; A24: (1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2))) = (1 / 2) * (((GoB f) * (1,1)) + (f /. 2)) by A10, MATRIX_2:6 .= (1 / 2) * ((f /. 4) + (f /. 2)) by A10, MATRIX_2:6 ; then A25: ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `1 = (1 / 2) * (((f /. 4) + (f /. 2)) `1) by TOPREAL3:4 .= (1 / 2) * (((f /. 4) `1) + ((f /. 2) `1)) by TOPREAL3:2 .= ((1 / 2) * ((f /. 4) `1)) + ((1 / 2) * ((f /. 2) `1)) ; LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def_1; hence LeftComp f = { p where p is Point of (TOP-REAL 2) : S1[p] } by A4, A7, A21, GOBOARD9:1; ::_thesis: RightComp f = { q where q is Point of (TOP-REAL 2) : ( W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) } A26: ((1 / 2) * (W-bound (L~ f))) + ((1 / 2) * (W-bound (L~ f))) = W-bound (L~ f) ; A27: ((1 / 2) * (E-bound (L~ f))) + ((1 / 2) * (E-bound (L~ f))) = E-bound (L~ f) ; A28: ((1 / 2) * (N-bound (L~ f))) + ((1 / 2) * (N-bound (L~ f))) = N-bound (L~ f) ; A29: (f /. 4) `1 = (W-min (L~ f)) `1 by SPRECT_1:86 .= W-bound (L~ f) by EUCLID:52 ; then (1 / 2) * ((f /. 4) `1) < (1 / 2) * (E-bound (L~ f)) by SPRECT_1:31, XREAL_1:68; then A30: ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `1 < E-bound (L~ f) by A27, A25, A22, XREAL_1:6; A31: ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `2 = (1 / 2) * (((f /. 4) + (f /. 2)) `2) by A24, TOPREAL3:4 .= (1 / 2) * (((f /. 4) `2) + ((f /. 2) `2)) by TOPREAL3:2 .= ((1 / 2) * ((f /. 4) `2)) + ((1 / 2) * ((f /. 2) `2)) ; Lc = Lc9 ; then Rc is a_component by A5, A1, JORDAN1:36; then A32: Rc9 is_a_component_of Lf ` by CONNSP_1:def_6; A33: (f /. 2) `2 = (N-max (L~ f)) `2 by SPRECT_1:84 .= N-bound (L~ f) by EUCLID:52 ; A34: (f /. 4) `2 = (S-min (L~ f)) `2 by SPRECT_1:86 .= S-bound (L~ f) by EUCLID:52 ; then (1 / 2) * ((f /. 4) `2) < (1 / 2) * (N-bound (L~ f)) by SPRECT_1:32, XREAL_1:68; then A35: ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `2 < N-bound (L~ f) by A28, A31, A33, XREAL_1:6; (1 / 2) * ((f /. 2) `2) > (1 / 2) * (S-bound (L~ f)) by A33, SPRECT_1:32, XREAL_1:68; then A36: S-bound (L~ f) < ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `2 by A6, A31, A34, XREAL_1:6; (1 / 2) * ((f /. 2) `1) > (1 / 2) * (W-bound (L~ f)) by A22, SPRECT_1:31, XREAL_1:68; then W-bound (L~ f) < ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2)))) `1 by A26, A25, A29, XREAL_1:6; then (1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,2))) in { q where q is Point of (TOP-REAL 2) : S2[q] } by A30, A36, A35; then A37: { q where q is Point of (TOP-REAL 2) : S2[q] } meets RightComp f by A23, A20, XBOOLE_0:3; RightComp f is_a_component_of (L~ f) ` by GOBOARD9:def_2; hence RightComp f = { q where q is Point of (TOP-REAL 2) : ( W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) } by A4, A32, A37, GOBOARD9:1; ::_thesis: verum end; registration cluster non empty non trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like V236( the U1 of (TOP-REAL 2)) special unfolded s.c.c. standard rectangular clockwise_oriented for FinSequence of the U1 of (TOP-REAL 2); existence ex b1 being rectangular special_circular_sequence st b1 is clockwise_oriented proof set C = the non empty compact non horizontal non vertical Subset of (TOP-REAL 2); SpStSeq the non empty compact non horizontal non vertical Subset of (TOP-REAL 2) is clockwise_oriented ; hence ex b1 being rectangular special_circular_sequence st b1 is clockwise_oriented ; ::_thesis: verum end; end; registration cluster non empty V236( the U1 of (TOP-REAL 2)) special unfolded s.c.c. rectangular -> rectangular clockwise_oriented for FinSequence of the U1 of (TOP-REAL 2); coherence for b1 being rectangular special_circular_sequence holds b1 is clockwise_oriented proof let f be rectangular special_circular_sequence; ::_thesis: f is clockwise_oriented ex D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) st f = SpStSeq D by SPRECT_1:def_2; hence f is clockwise_oriented ; ::_thesis: verum end; end; theorem :: SPRECT_3:38 for f being rectangular special_circular_sequence for g being S-Sequence_in_R2 st g /. 1 in LeftComp f & g /. (len g) in RightComp f holds Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) <> NW-corner (L~ f) proof let f be rectangular special_circular_sequence; ::_thesis: for g being S-Sequence_in_R2 st g /. 1 in LeftComp f & g /. (len g) in RightComp f holds Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) <> NW-corner (L~ f) let g be S-Sequence_in_R2; ::_thesis: ( g /. 1 in LeftComp f & g /. (len g) in RightComp f implies Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) <> NW-corner (L~ f) ) assume that A1: g /. 1 in LeftComp f and A2: g /. (len g) in RightComp f ; ::_thesis: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) <> NW-corner (L~ f) A3: L~ f meets L~ g by A1, A2, Th33; assume A4: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) = NW-corner (L~ f) ; ::_thesis: contradiction set nw = NW-corner (L~ f); set inw = Index ((NW-corner (L~ f)),g); A5: len g in dom g by FINSEQ_5:6; then A6: g . (len g) = g /. (len g) by PARTFUN1:def_6; A7: 1 <= (Index ((NW-corner (L~ f)),g)) + 1 by NAT_1:11; L~ g is_an_arc_of g /. 1,g /. (len g) by TOPREAL1:25; then A8: NW-corner (L~ f) in (L~ g) /\ (L~ f) by A3, A4, JORDAN5C:def_2; then A9: NW-corner (L~ f) in L~ g by XBOOLE_0:def_4; then A10: 1 <= Index ((NW-corner (L~ f)),g) by JORDAN3:8; A11: NW-corner (L~ f) in LSeg (g,(Index ((NW-corner (L~ f)),g))) by A9, JORDAN3:9; A12: Index ((NW-corner (L~ f)),g) < len g by A9, JORDAN3:8; then A13: (Index ((NW-corner (L~ f)),g)) + 1 <= len g by NAT_1:13; then A14: (Index ((NW-corner (L~ f)),g)) + 1 in dom g by A7, FINSEQ_3:25; A15: L~ f misses RightComp f by Th25; A16: now__::_thesis:_not_NW-corner_(L~_f)_<>_g_._((Index_((NW-corner_(L~_f)),g))_+_1) A17: len g >= 1 by A13, A7, XXREAL_0:2; assume NW-corner (L~ f) <> g . ((Index ((NW-corner (L~ f)),g)) + 1) ; ::_thesis: contradiction then A18: NW-corner (L~ f) <> g /. ((Index ((NW-corner (L~ f)),g)) + 1) by A14, PARTFUN1:def_6; percases ( g /. ((Index ((NW-corner (L~ f)),g)) + 1) in L~ f or not g /. ((Index ((NW-corner (L~ f)),g)) + 1) in L~ f ) ; supposeA19: g /. ((Index ((NW-corner (L~ f)),g)) + 1) in L~ f ; ::_thesis: contradiction then (Index ((NW-corner (L~ f)),g)) + 1 <> len g by A2, A15, XBOOLE_0:3; then (Index ((NW-corner (L~ f)),g)) + 1 < len g by A13, XXREAL_0:1; then A20: ((Index ((NW-corner (L~ f)),g)) + 1) + 1 <= len g by NAT_1:13; then g /. ((Index ((NW-corner (L~ f)),g)) + 1) in LSeg (g,((Index ((NW-corner (L~ f)),g)) + 1)) by A7, TOPREAL1:21; then Index ((NW-corner (L~ f)),g) >= (Index ((NW-corner (L~ f)),g)) + 1 by A3, A4, A10, A13, A11, A7, A18, A19, A20, JORDAN5C:28; hence contradiction by XREAL_1:29; ::_thesis: verum end; supposeA21: not g /. ((Index ((NW-corner (L~ f)),g)) + 1) in L~ f ; ::_thesis: contradiction A22: now__::_thesis:_not_g_/._((Index_((NW-corner_(L~_f)),g))_+_1)_in_RightComp_f assume A23: g /. ((Index ((NW-corner (L~ f)),g)) + 1) in RightComp f ; ::_thesis: contradiction RightComp f = { q where q is Point of (TOP-REAL 2) : ( W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) } by Th37; then A24: ex q being Point of (TOP-REAL 2) st ( g /. ((Index ((NW-corner (L~ f)),g)) + 1) = q & W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) by A23; A25: ( LSeg (g,(Index ((NW-corner (L~ f)),g))) is vertical or LSeg (g,(Index ((NW-corner (L~ f)),g))) is horizontal ) by SPPOL_1:19; LSeg (g,(Index ((NW-corner (L~ f)),g))) = LSeg ((g /. (Index ((NW-corner (L~ f)),g))),(g /. ((Index ((NW-corner (L~ f)),g)) + 1))) by A10, A13, TOPREAL1:def_3; then ( (g /. ((Index ((NW-corner (L~ f)),g)) + 1)) `1 = (NW-corner (L~ f)) `1 or (g /. ((Index ((NW-corner (L~ f)),g)) + 1)) `2 = (NW-corner (L~ f)) `2 ) by A11, A25, SPPOL_1:40, SPPOL_1:41; hence contradiction by A24, EUCLID:52; ::_thesis: verum end; then reconsider m = mid (g,((Index ((NW-corner (L~ f)),g)) + 1),(len g)) as S-Sequence_in_R2 by A2, A13, A7, A17, JORDAN3:6; A26: (Index ((NW-corner (L~ f)),g)) + 1 < len g by A2, A13, A22, XXREAL_0:1; g /. ((Index ((NW-corner (L~ f)),g)) + 1) in (L~ f) ` by A21, SUBSET_1:29; then g /. ((Index ((NW-corner (L~ f)),g)) + 1) in (LeftComp f) \/ (RightComp f) by GOBRD12:10; then g /. ((Index ((NW-corner (L~ f)),g)) + 1) in LeftComp f by A22, XBOOLE_0:def_3; then A27: m /. 1 in LeftComp f by A5, A14, SPRECT_2:8; m /. (len m) in RightComp f by A2, A5, A14, SPRECT_2:9; then L~ f meets L~ m by A27, Th33; then consider q being set such that A28: q in L~ f and A29: q in L~ m by XBOOLE_0:3; reconsider q = q as Point of (TOP-REAL 2) by A29; consider i being Element of NAT such that A30: 1 <= i and A31: i + 1 <= len m and A32: q in LSeg (m,i) by A29, SPPOL_2:13; set j = (i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1; A33: (i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1 = ((i + (Index ((NW-corner (L~ f)),g))) + 1) -' 1 .= i + (Index ((NW-corner (L~ f)),g)) by NAT_D:34 ; A34: len m = ((len g) -' ((Index ((NW-corner (L~ f)),g)) + 1)) + 1 by A13, A7, JORDAN4:8; then len m = (len g) -' (Index ((NW-corner (L~ f)),g)) by A9, JORDAN3:8, NAT_2:7; then (len m) + (Index ((NW-corner (L~ f)),g)) = len g by A12, XREAL_1:235; then (i + 1) + (Index ((NW-corner (L~ f)),g)) <= len g by A31, XREAL_1:6; then A35: ((i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1) + 1 <= len g by A33; i < len m by A31, NAT_1:13; then A36: LSeg (m,i) = LSeg (g,((i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1)) by A7, A26, A30, A34, JORDAN4:19; A37: (i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1 >= (Index ((NW-corner (L~ f)),g)) + 1 by A30, A33, XREAL_1:6; A38: now__::_thesis:_not_NW-corner_(L~_f)_=_q assume NW-corner (L~ f) = q ; ::_thesis: contradiction then A39: NW-corner (L~ f) in (LSeg (g,(Index ((NW-corner (L~ f)),g)))) /\ (LSeg (g,((i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1))) by A11, A32, A36, XBOOLE_0:def_4; then A40: LSeg (g,(Index ((NW-corner (L~ f)),g))) meets LSeg (g,((i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1)) by XBOOLE_0:4; percases ( (Index ((NW-corner (L~ f)),g)) + 1 = (i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1 or (Index ((NW-corner (L~ f)),g)) + 1 < (i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1 ) by A37, XXREAL_0:1; supposeA41: (Index ((NW-corner (L~ f)),g)) + 1 = (i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1 ; ::_thesis: contradiction ((Index ((NW-corner (L~ f)),g)) + 1) + 1 <= len g by A26, NAT_1:13; then (Index ((NW-corner (L~ f)),g)) + (1 + 1) <= len g ; then (LSeg (g,(Index ((NW-corner (L~ f)),g)))) /\ (LSeg (g,((Index ((NW-corner (L~ f)),g)) + 1))) = {(g /. ((Index ((NW-corner (L~ f)),g)) + 1))} by A10, TOPREAL1:def_6; hence contradiction by A18, A39, A41, TARSKI:def_1; ::_thesis: verum end; suppose (Index ((NW-corner (L~ f)),g)) + 1 < (i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1 ; ::_thesis: contradiction hence contradiction by A40, TOPREAL1:def_7; ::_thesis: verum end; end; end; Index ((NW-corner (L~ f)),g) >= 0 by NAT_1:2; then 0 + 1 <= (i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1 by A30, A33, XREAL_1:7; then Index ((NW-corner (L~ f)),g) >= (i + ((Index ((NW-corner (L~ f)),g)) + 1)) -' 1 by A3, A4, A10, A13, A11, A28, A32, A36, A35, A38, JORDAN5C:28; then Index ((NW-corner (L~ f)),g) >= (Index ((NW-corner (L~ f)),g)) + 1 by A37, XXREAL_0:2; hence contradiction by XREAL_1:29; ::_thesis: verum end; end; end; NW-corner (L~ f) in L~ f by A8, XBOOLE_0:def_4; then NW-corner (L~ f) <> g . (len g) by A2, A15, A6, XBOOLE_0:3; then A42: (Index ((NW-corner (L~ f)),g)) + 1 < len g by A13, A16, XXREAL_0:1; then A43: ((Index ((NW-corner (L~ f)),g)) + 1) + 1 <= len g by NAT_1:13; then g /. ((Index ((NW-corner (L~ f)),g)) + 1) in LSeg (g,((Index ((NW-corner (L~ f)),g)) + 1)) by A7, TOPREAL1:21; then A44: NW-corner (L~ f) in LSeg (g,((Index ((NW-corner (L~ f)),g)) + 1)) by A14, A16, PARTFUN1:def_6; A45: 1 <= ((Index ((NW-corner (L~ f)),g)) + 1) + 1 by NAT_1:11; then A46: len g >= 1 by A43, XXREAL_0:2; A47: ((Index ((NW-corner (L~ f)),g)) + 1) + 1 in dom g by A43, A45, FINSEQ_3:25; (Index ((NW-corner (L~ f)),g)) + 1 < ((Index ((NW-corner (L~ f)),g)) + 1) + 1 by NAT_1:13; then A48: NW-corner (L~ f) <> g . (((Index ((NW-corner (L~ f)),g)) + 1) + 1) by A14, A16, A47, FUNCT_1:def_4; then A49: NW-corner (L~ f) <> g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) by A47, PARTFUN1:def_6; percases ( g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in L~ f or not g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in L~ f ) ; supposeA50: g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in L~ f ; ::_thesis: contradiction A51: NW-corner (L~ f) <> g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) by A47, A48, PARTFUN1:def_6; ((Index ((NW-corner (L~ f)),g)) + 1) + 1 <> len g by A2, A15, A50, XBOOLE_0:3; then ((Index ((NW-corner (L~ f)),g)) + 1) + 1 < len g by A43, XXREAL_0:1; then A52: (((Index ((NW-corner (L~ f)),g)) + 1) + 1) + 1 <= len g by NAT_1:13; then g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in LSeg (g,(((Index ((NW-corner (L~ f)),g)) + 1) + 1)) by A45, TOPREAL1:21; then (Index ((NW-corner (L~ f)),g)) + 1 >= ((Index ((NW-corner (L~ f)),g)) + 1) + 1 by A3, A4, A7, A43, A45, A44, A50, A52, A51, JORDAN5C:28; hence contradiction by XREAL_1:29; ::_thesis: verum end; supposeA53: not g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in L~ f ; ::_thesis: contradiction A54: now__::_thesis:_not_g_/._(((Index_((NW-corner_(L~_f)),g))_+_1)_+_1)_in_RightComp_f assume A55: g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in RightComp f ; ::_thesis: contradiction RightComp f = { q where q is Point of (TOP-REAL 2) : ( W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) } by Th37; then A56: ex q being Point of (TOP-REAL 2) st ( g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) = q & W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) by A55; A57: ( LSeg (g,((Index ((NW-corner (L~ f)),g)) + 1)) is vertical or LSeg (g,((Index ((NW-corner (L~ f)),g)) + 1)) is horizontal ) by SPPOL_1:19; LSeg (g,((Index ((NW-corner (L~ f)),g)) + 1)) = LSeg ((g /. ((Index ((NW-corner (L~ f)),g)) + 1)),(g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1))) by A7, A43, TOPREAL1:def_3; then ( (g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) `1 = (NW-corner (L~ f)) `1 or (g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) `2 = (NW-corner (L~ f)) `2 ) by A44, A57, SPPOL_1:40, SPPOL_1:41; hence contradiction by A56, EUCLID:52; ::_thesis: verum end; then reconsider m = mid (g,(((Index ((NW-corner (L~ f)),g)) + 1) + 1),(len g)) as S-Sequence_in_R2 by A2, A43, A45, A46, JORDAN3:6; A58: ((Index ((NW-corner (L~ f)),g)) + 1) + 1 < len g by A2, A43, A54, XXREAL_0:1; g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in (L~ f) ` by A53, SUBSET_1:29; then g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in (LeftComp f) \/ (RightComp f) by GOBRD12:10; then g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1) in LeftComp f by A54, XBOOLE_0:def_3; then A59: m /. 1 in LeftComp f by A5, A47, SPRECT_2:8; m /. (len m) in RightComp f by A2, A5, A47, SPRECT_2:9; then L~ f meets L~ m by A59, Th33; then consider q being set such that A60: q in L~ f and A61: q in L~ m by XBOOLE_0:3; reconsider q = q as Point of (TOP-REAL 2) by A61; consider i being Element of NAT such that A62: 1 <= i and A63: i + 1 <= len m and A64: q in LSeg (m,i) by A61, SPPOL_2:13; set j = (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1; A65: len m = ((len g) -' (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) + 1 by A43, A45, JORDAN4:8; then len m = (len g) -' ((Index ((NW-corner (L~ f)),g)) + 1) by A42, NAT_2:7; then (len m) + ((Index ((NW-corner (L~ f)),g)) + 1) = len g by A13, XREAL_1:235; then (i + 1) + ((Index ((NW-corner (L~ f)),g)) + 1) <= len g by A63, XREAL_1:6; then A66: ((i + 1) + (Index ((NW-corner (L~ f)),g))) + 1 <= len g ; i < len m by A63, NAT_1:13; then A67: LSeg (m,i) = LSeg (g,((i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1)) by A45, A58, A62, A65, JORDAN4:19; A68: (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1 = (((i + (Index ((NW-corner (L~ f)),g))) + 1) + 1) -' 1 .= (i + (Index ((NW-corner (L~ f)),g))) + 1 by NAT_D:34 ; then (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1 = i + ((Index ((NW-corner (L~ f)),g)) + 1) ; then A69: (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1 >= ((Index ((NW-corner (L~ f)),g)) + 1) + 1 by A62, XREAL_1:6; A70: now__::_thesis:_not_NW-corner_(L~_f)_=_q assume NW-corner (L~ f) = q ; ::_thesis: contradiction then A71: NW-corner (L~ f) in (LSeg (g,((Index ((NW-corner (L~ f)),g)) + 1))) /\ (LSeg (g,((i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1))) by A44, A64, A67, XBOOLE_0:def_4; then A72: LSeg (g,((Index ((NW-corner (L~ f)),g)) + 1)) meets LSeg (g,((i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1)) by XBOOLE_0:4; percases ( ((Index ((NW-corner (L~ f)),g)) + 1) + 1 = (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1 or ((Index ((NW-corner (L~ f)),g)) + 1) + 1 < (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1 ) by A69, XXREAL_0:1; supposeA73: ((Index ((NW-corner (L~ f)),g)) + 1) + 1 = (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1 ; ::_thesis: contradiction (((Index ((NW-corner (L~ f)),g)) + 1) + 1) + 1 <= len g by A58, NAT_1:13; then ((Index ((NW-corner (L~ f)),g)) + 1) + (1 + 1) <= len g ; then (LSeg (g,((Index ((NW-corner (L~ f)),g)) + 1))) /\ (LSeg (g,(((Index ((NW-corner (L~ f)),g)) + 1) + 1))) = {(g /. (((Index ((NW-corner (L~ f)),g)) + 1) + 1))} by A7, TOPREAL1:def_6; hence contradiction by A49, A71, A73, TARSKI:def_1; ::_thesis: verum end; suppose ((Index ((NW-corner (L~ f)),g)) + 1) + 1 < (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1 ; ::_thesis: contradiction hence contradiction by A72, TOPREAL1:def_7; ::_thesis: verum end; end; end; 0 + 1 <= (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1 by A68, NAT_1:11; then (Index ((NW-corner (L~ f)),g)) + 1 >= (i + (((Index ((NW-corner (L~ f)),g)) + 1) + 1)) -' 1 by A3, A4, A7, A43, A44, A60, A64, A67, A68, A66, A70, JORDAN5C:28; then (Index ((NW-corner (L~ f)),g)) + 1 >= ((Index ((NW-corner (L~ f)),g)) + 1) + 1 by A69, XXREAL_0:2; hence contradiction by XREAL_1:29; ::_thesis: verum end; end; end; theorem :: SPRECT_3:39 for f being rectangular special_circular_sequence for g being S-Sequence_in_R2 st g /. 1 in LeftComp f & g /. (len g) in RightComp f holds Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) <> SE-corner (L~ f) proof let f be rectangular special_circular_sequence; ::_thesis: for g being S-Sequence_in_R2 st g /. 1 in LeftComp f & g /. (len g) in RightComp f holds Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) <> SE-corner (L~ f) let g be S-Sequence_in_R2; ::_thesis: ( g /. 1 in LeftComp f & g /. (len g) in RightComp f implies Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) <> SE-corner (L~ f) ) assume that A1: g /. 1 in LeftComp f and A2: g /. (len g) in RightComp f ; ::_thesis: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) <> SE-corner (L~ f) A3: L~ f meets L~ g by A1, A2, Th33; assume A4: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) = SE-corner (L~ f) ; ::_thesis: contradiction set se = SE-corner (L~ f); set ise = Index ((SE-corner (L~ f)),g); A5: len g in dom g by FINSEQ_5:6; then A6: g . (len g) = g /. (len g) by PARTFUN1:def_6; A7: 1 <= (Index ((SE-corner (L~ f)),g)) + 1 by NAT_1:11; L~ g is_an_arc_of g /. 1,g /. (len g) by TOPREAL1:25; then A8: SE-corner (L~ f) in (L~ g) /\ (L~ f) by A3, A4, JORDAN5C:def_2; then A9: SE-corner (L~ f) in L~ g by XBOOLE_0:def_4; then A10: 1 <= Index ((SE-corner (L~ f)),g) by JORDAN3:8; A11: SE-corner (L~ f) in LSeg (g,(Index ((SE-corner (L~ f)),g))) by A9, JORDAN3:9; A12: Index ((SE-corner (L~ f)),g) < len g by A9, JORDAN3:8; then A13: (Index ((SE-corner (L~ f)),g)) + 1 <= len g by NAT_1:13; then A14: (Index ((SE-corner (L~ f)),g)) + 1 in dom g by A7, FINSEQ_3:25; A15: L~ f misses RightComp f by Th25; A16: now__::_thesis:_not_SE-corner_(L~_f)_<>_g_._((Index_((SE-corner_(L~_f)),g))_+_1) A17: len g >= 1 by A13, A7, XXREAL_0:2; assume SE-corner (L~ f) <> g . ((Index ((SE-corner (L~ f)),g)) + 1) ; ::_thesis: contradiction then A18: SE-corner (L~ f) <> g /. ((Index ((SE-corner (L~ f)),g)) + 1) by A14, PARTFUN1:def_6; percases ( g /. ((Index ((SE-corner (L~ f)),g)) + 1) in L~ f or not g /. ((Index ((SE-corner (L~ f)),g)) + 1) in L~ f ) ; supposeA19: g /. ((Index ((SE-corner (L~ f)),g)) + 1) in L~ f ; ::_thesis: contradiction then (Index ((SE-corner (L~ f)),g)) + 1 <> len g by A2, A15, XBOOLE_0:3; then (Index ((SE-corner (L~ f)),g)) + 1 < len g by A13, XXREAL_0:1; then A20: ((Index ((SE-corner (L~ f)),g)) + 1) + 1 <= len g by NAT_1:13; then g /. ((Index ((SE-corner (L~ f)),g)) + 1) in LSeg (g,((Index ((SE-corner (L~ f)),g)) + 1)) by A7, TOPREAL1:21; then Index ((SE-corner (L~ f)),g) >= (Index ((SE-corner (L~ f)),g)) + 1 by A3, A4, A10, A13, A11, A7, A18, A19, A20, JORDAN5C:28; hence contradiction by XREAL_1:29; ::_thesis: verum end; supposeA21: not g /. ((Index ((SE-corner (L~ f)),g)) + 1) in L~ f ; ::_thesis: contradiction A22: now__::_thesis:_not_g_/._((Index_((SE-corner_(L~_f)),g))_+_1)_in_RightComp_f assume A23: g /. ((Index ((SE-corner (L~ f)),g)) + 1) in RightComp f ; ::_thesis: contradiction RightComp f = { q where q is Point of (TOP-REAL 2) : ( W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) } by Th37; then A24: ex q being Point of (TOP-REAL 2) st ( g /. ((Index ((SE-corner (L~ f)),g)) + 1) = q & W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) by A23; A25: ( LSeg (g,(Index ((SE-corner (L~ f)),g))) is vertical or LSeg (g,(Index ((SE-corner (L~ f)),g))) is horizontal ) by SPPOL_1:19; LSeg (g,(Index ((SE-corner (L~ f)),g))) = LSeg ((g /. (Index ((SE-corner (L~ f)),g))),(g /. ((Index ((SE-corner (L~ f)),g)) + 1))) by A10, A13, TOPREAL1:def_3; then ( (g /. ((Index ((SE-corner (L~ f)),g)) + 1)) `1 = (SE-corner (L~ f)) `1 or (g /. ((Index ((SE-corner (L~ f)),g)) + 1)) `2 = (SE-corner (L~ f)) `2 ) by A11, A25, SPPOL_1:40, SPPOL_1:41; hence contradiction by A24, EUCLID:52; ::_thesis: verum end; then reconsider m = mid (g,((Index ((SE-corner (L~ f)),g)) + 1),(len g)) as S-Sequence_in_R2 by A2, A13, A7, A17, JORDAN3:6; A26: (Index ((SE-corner (L~ f)),g)) + 1 < len g by A2, A13, A22, XXREAL_0:1; g /. ((Index ((SE-corner (L~ f)),g)) + 1) in (L~ f) ` by A21, SUBSET_1:29; then g /. ((Index ((SE-corner (L~ f)),g)) + 1) in (LeftComp f) \/ (RightComp f) by GOBRD12:10; then g /. ((Index ((SE-corner (L~ f)),g)) + 1) in LeftComp f by A22, XBOOLE_0:def_3; then A27: m /. 1 in LeftComp f by A5, A14, SPRECT_2:8; m /. (len m) in RightComp f by A2, A5, A14, SPRECT_2:9; then L~ f meets L~ m by A27, Th33; then consider q being set such that A28: q in L~ f and A29: q in L~ m by XBOOLE_0:3; reconsider q = q as Point of (TOP-REAL 2) by A29; consider i being Element of NAT such that A30: 1 <= i and A31: i + 1 <= len m and A32: q in LSeg (m,i) by A29, SPPOL_2:13; set j = (i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1; A33: (i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1 = ((i + (Index ((SE-corner (L~ f)),g))) + 1) -' 1 .= i + (Index ((SE-corner (L~ f)),g)) by NAT_D:34 ; A34: len m = ((len g) -' ((Index ((SE-corner (L~ f)),g)) + 1)) + 1 by A13, A7, JORDAN4:8; then len m = (len g) -' (Index ((SE-corner (L~ f)),g)) by A9, JORDAN3:8, NAT_2:7; then (len m) + (Index ((SE-corner (L~ f)),g)) = len g by A12, XREAL_1:235; then (i + 1) + (Index ((SE-corner (L~ f)),g)) <= len g by A31, XREAL_1:6; then A35: ((i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1) + 1 <= len g by A33; i < len m by A31, NAT_1:13; then A36: LSeg (m,i) = LSeg (g,((i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1)) by A7, A26, A30, A34, JORDAN4:19; A37: (i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1 >= (Index ((SE-corner (L~ f)),g)) + 1 by A30, A33, XREAL_1:6; A38: now__::_thesis:_not_SE-corner_(L~_f)_=_q assume SE-corner (L~ f) = q ; ::_thesis: contradiction then A39: SE-corner (L~ f) in (LSeg (g,(Index ((SE-corner (L~ f)),g)))) /\ (LSeg (g,((i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1))) by A11, A32, A36, XBOOLE_0:def_4; then A40: LSeg (g,(Index ((SE-corner (L~ f)),g))) meets LSeg (g,((i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1)) by XBOOLE_0:4; percases ( (Index ((SE-corner (L~ f)),g)) + 1 = (i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1 or (Index ((SE-corner (L~ f)),g)) + 1 < (i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1 ) by A37, XXREAL_0:1; supposeA41: (Index ((SE-corner (L~ f)),g)) + 1 = (i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1 ; ::_thesis: contradiction ((Index ((SE-corner (L~ f)),g)) + 1) + 1 <= len g by A26, NAT_1:13; then (Index ((SE-corner (L~ f)),g)) + (1 + 1) <= len g ; then (LSeg (g,(Index ((SE-corner (L~ f)),g)))) /\ (LSeg (g,((Index ((SE-corner (L~ f)),g)) + 1))) = {(g /. ((Index ((SE-corner (L~ f)),g)) + 1))} by A10, TOPREAL1:def_6; hence contradiction by A18, A39, A41, TARSKI:def_1; ::_thesis: verum end; suppose (Index ((SE-corner (L~ f)),g)) + 1 < (i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1 ; ::_thesis: contradiction hence contradiction by A40, TOPREAL1:def_7; ::_thesis: verum end; end; end; Index ((SE-corner (L~ f)),g) >= 0 by NAT_1:2; then 0 + 1 <= (i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1 by A30, A33, XREAL_1:7; then Index ((SE-corner (L~ f)),g) >= (i + ((Index ((SE-corner (L~ f)),g)) + 1)) -' 1 by A3, A4, A10, A13, A11, A28, A32, A36, A35, A38, JORDAN5C:28; then Index ((SE-corner (L~ f)),g) >= (Index ((SE-corner (L~ f)),g)) + 1 by A37, XXREAL_0:2; hence contradiction by XREAL_1:29; ::_thesis: verum end; end; end; SE-corner (L~ f) in L~ f by A8, XBOOLE_0:def_4; then SE-corner (L~ f) <> g . (len g) by A2, A15, A6, XBOOLE_0:3; then A42: (Index ((SE-corner (L~ f)),g)) + 1 < len g by A13, A16, XXREAL_0:1; then A43: ((Index ((SE-corner (L~ f)),g)) + 1) + 1 <= len g by NAT_1:13; then g /. ((Index ((SE-corner (L~ f)),g)) + 1) in LSeg (g,((Index ((SE-corner (L~ f)),g)) + 1)) by A7, TOPREAL1:21; then A44: SE-corner (L~ f) in LSeg (g,((Index ((SE-corner (L~ f)),g)) + 1)) by A14, A16, PARTFUN1:def_6; A45: 1 <= ((Index ((SE-corner (L~ f)),g)) + 1) + 1 by NAT_1:11; then A46: len g >= 1 by A43, XXREAL_0:2; A47: ((Index ((SE-corner (L~ f)),g)) + 1) + 1 in dom g by A43, A45, FINSEQ_3:25; (Index ((SE-corner (L~ f)),g)) + 1 < ((Index ((SE-corner (L~ f)),g)) + 1) + 1 by NAT_1:13; then A48: SE-corner (L~ f) <> g . (((Index ((SE-corner (L~ f)),g)) + 1) + 1) by A14, A16, A47, FUNCT_1:def_4; then A49: SE-corner (L~ f) <> g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) by A47, PARTFUN1:def_6; percases ( g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) in L~ f or not g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) in L~ f ) ; supposeA50: g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) in L~ f ; ::_thesis: contradiction A51: SE-corner (L~ f) <> g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) by A47, A48, PARTFUN1:def_6; ((Index ((SE-corner (L~ f)),g)) + 1) + 1 <> len g by A2, A15, A50, XBOOLE_0:3; then ((Index ((SE-corner (L~ f)),g)) + 1) + 1 < len g by A43, XXREAL_0:1; then A52: (((Index ((SE-corner (L~ f)),g)) + 1) + 1) + 1 <= len g by NAT_1:13; then g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) in LSeg (g,(((Index ((SE-corner (L~ f)),g)) + 1) + 1)) by A45, TOPREAL1:21; then (Index ((SE-corner (L~ f)),g)) + 1 >= ((Index ((SE-corner (L~ f)),g)) + 1) + 1 by A3, A4, A7, A43, A45, A44, A50, A52, A51, JORDAN5C:28; hence contradiction by XREAL_1:29; ::_thesis: verum end; supposeA53: not g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) in L~ f ; ::_thesis: contradiction A54: now__::_thesis:_not_g_/._(((Index_((SE-corner_(L~_f)),g))_+_1)_+_1)_in_RightComp_f assume A55: g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) in RightComp f ; ::_thesis: contradiction RightComp f = { q where q is Point of (TOP-REAL 2) : ( W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) } by Th37; then A56: ex q being Point of (TOP-REAL 2) st ( g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) = q & W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) & S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) ) by A55; A57: ( LSeg (g,((Index ((SE-corner (L~ f)),g)) + 1)) is vertical or LSeg (g,((Index ((SE-corner (L~ f)),g)) + 1)) is horizontal ) by SPPOL_1:19; LSeg (g,((Index ((SE-corner (L~ f)),g)) + 1)) = LSeg ((g /. ((Index ((SE-corner (L~ f)),g)) + 1)),(g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1))) by A7, A43, TOPREAL1:def_3; then ( (g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) `1 = (SE-corner (L~ f)) `1 or (g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) `2 = (SE-corner (L~ f)) `2 ) by A44, A57, SPPOL_1:40, SPPOL_1:41; hence contradiction by A56, EUCLID:52; ::_thesis: verum end; then reconsider m = mid (g,(((Index ((SE-corner (L~ f)),g)) + 1) + 1),(len g)) as S-Sequence_in_R2 by A2, A43, A45, A46, JORDAN3:6; A58: ((Index ((SE-corner (L~ f)),g)) + 1) + 1 < len g by A2, A43, A54, XXREAL_0:1; g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) in (L~ f) ` by A53, SUBSET_1:29; then g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) in (LeftComp f) \/ (RightComp f) by GOBRD12:10; then g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1) in LeftComp f by A54, XBOOLE_0:def_3; then A59: m /. 1 in LeftComp f by A5, A47, SPRECT_2:8; m /. (len m) in RightComp f by A2, A5, A47, SPRECT_2:9; then L~ f meets L~ m by A59, Th33; then consider q being set such that A60: q in L~ f and A61: q in L~ m by XBOOLE_0:3; reconsider q = q as Point of (TOP-REAL 2) by A61; consider i being Element of NAT such that A62: 1 <= i and A63: i + 1 <= len m and A64: q in LSeg (m,i) by A61, SPPOL_2:13; set j = (i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1; A65: len m = ((len g) -' (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) + 1 by A43, A45, JORDAN4:8; then len m = (len g) -' ((Index ((SE-corner (L~ f)),g)) + 1) by A42, NAT_2:7; then (len m) + ((Index ((SE-corner (L~ f)),g)) + 1) = len g by A13, XREAL_1:235; then (i + 1) + ((Index ((SE-corner (L~ f)),g)) + 1) <= len g by A63, XREAL_1:6; then A66: ((i + 1) + (Index ((SE-corner (L~ f)),g))) + 1 <= len g ; i < len m by A63, NAT_1:13; then A67: LSeg (m,i) = LSeg (g,((i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1)) by A45, A58, A62, A65, JORDAN4:19; A68: (i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1 = (((i + (Index ((SE-corner (L~ f)),g))) + 1) + 1) -' 1 .= (i + (Index ((SE-corner (L~ f)),g))) + 1 by NAT_D:34 ; then (i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1 = i + ((Index ((SE-corner (L~ f)),g)) + 1) ; then A69: (i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1 >= ((Index ((SE-corner (L~ f)),g)) + 1) + 1 by A62, XREAL_1:6; A70: now__::_thesis:_not_SE-corner_(L~_f)_=_q assume SE-corner (L~ f) = q ; ::_thesis: contradiction then A71: SE-corner (L~ f) in (LSeg (g,((Index ((SE-corner (L~ f)),g)) + 1))) /\ (LSeg (g,((i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1))) by A44, A64, A67, XBOOLE_0:def_4; then A72: LSeg (g,((Index ((SE-corner (L~ f)),g)) + 1)) meets LSeg (g,((i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1)) by XBOOLE_0:4; percases ( ((Index ((SE-corner (L~ f)),g)) + 1) + 1 = (i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1 or ((Index ((SE-corner (L~ f)),g)) + 1) + 1 < (i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1 ) by A69, XXREAL_0:1; supposeA73: ((Index ((SE-corner (L~ f)),g)) + 1) + 1 = (i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1 ; ::_thesis: contradiction (((Index ((SE-corner (L~ f)),g)) + 1) + 1) + 1 <= len g by A58, NAT_1:13; then ((Index ((SE-corner (L~ f)),g)) + 1) + (1 + 1) <= len g ; then (LSeg (g,((Index ((SE-corner (L~ f)),g)) + 1))) /\ (LSeg (g,(((Index ((SE-corner (L~ f)),g)) + 1) + 1))) = {(g /. (((Index ((SE-corner (L~ f)),g)) + 1) + 1))} by A7, TOPREAL1:def_6; hence contradiction by A49, A71, A73, TARSKI:def_1; ::_thesis: verum end; suppose ((Index ((SE-corner (L~ f)),g)) + 1) + 1 < (i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1 ; ::_thesis: contradiction hence contradiction by A72, TOPREAL1:def_7; ::_thesis: verum end; end; end; 0 + 1 <= (i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1 by A68, NAT_1:11; then (Index ((SE-corner (L~ f)),g)) + 1 >= (i + (((Index ((SE-corner (L~ f)),g)) + 1) + 1)) -' 1 by A3, A4, A7, A43, A44, A60, A64, A67, A68, A66, A70, JORDAN5C:28; then (Index ((SE-corner (L~ f)),g)) + 1 >= ((Index ((SE-corner (L~ f)),g)) + 1) + 1 by A69, XXREAL_0:2; hence contradiction by XREAL_1:29; ::_thesis: verum end; end; end; theorem Th40: :: SPRECT_3:40 for f being rectangular special_circular_sequence for p being Point of (TOP-REAL 2) st ( W-bound (L~ f) > p `1 or p `1 > E-bound (L~ f) or S-bound (L~ f) > p `2 or p `2 > N-bound (L~ f) ) holds p in LeftComp f proof let f be rectangular special_circular_sequence; ::_thesis: for p being Point of (TOP-REAL 2) st ( W-bound (L~ f) > p `1 or p `1 > E-bound (L~ f) or S-bound (L~ f) > p `2 or p `2 > N-bound (L~ f) ) holds p in LeftComp f let p be Point of (TOP-REAL 2); ::_thesis: ( ( W-bound (L~ f) > p `1 or p `1 > E-bound (L~ f) or S-bound (L~ f) > p `2 or p `2 > N-bound (L~ f) ) implies p in LeftComp f ) LeftComp f = { q where q is Point of (TOP-REAL 2) : ( not W-bound (L~ f) <= q `1 or not q `1 <= E-bound (L~ f) or not S-bound (L~ f) <= q `2 or not q `2 <= N-bound (L~ f) ) } by Th37; hence ( ( W-bound (L~ f) > p `1 or p `1 > E-bound (L~ f) or S-bound (L~ f) > p `2 or p `2 > N-bound (L~ f) ) implies p in LeftComp f ) ; ::_thesis: verum end; theorem :: SPRECT_3:41 for f being non constant standard clockwise_oriented special_circular_sequence st f /. 1 = N-min (L~ f) holds LeftComp (SpStSeq (L~ f)) c= LeftComp f proof let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( f /. 1 = N-min (L~ f) implies LeftComp (SpStSeq (L~ f)) c= LeftComp f ) assume A1: f /. 1 = N-min (L~ f) ; ::_thesis: LeftComp (SpStSeq (L~ f)) c= LeftComp f defpred S1[ Element of (TOP-REAL 2)] means $1 `2 < S-bound (L~ f); reconsider P1 = { p where p is Point of (TOP-REAL 2) : S1[p] } as Subset of (TOP-REAL 2) from DOMAIN_1:sch_7(); defpred S2[ Element of (TOP-REAL 2)] means $1 `2 > N-bound (L~ f); reconsider P2 = { p where p is Point of (TOP-REAL 2) : S2[p] } as Subset of (TOP-REAL 2) from DOMAIN_1:sch_7(); defpred S3[ Element of (TOP-REAL 2)] means $1 `1 > E-bound (L~ f); reconsider P3 = { p where p is Point of (TOP-REAL 2) : S3[p] } as Subset of (TOP-REAL 2) from DOMAIN_1:sch_7(); defpred S4[ Element of (TOP-REAL 2)] means $1 `1 < W-bound (L~ f); reconsider P4 = { p where p is Point of (TOP-REAL 2) : S4[p] } as Subset of (TOP-REAL 2) from DOMAIN_1:sch_7(); A2: W-bound (L~ (SpStSeq (L~ f))) = W-bound (L~ f) by SPRECT_1:58; for p being Point of (TOP-REAL 2) st p in P2 holds p `2 > ((GoB f) * (1,(width (GoB f)))) `2 proof let p be Point of (TOP-REAL 2); ::_thesis: ( p in P2 implies p `2 > ((GoB f) * (1,(width (GoB f)))) `2 ) assume p in P2 ; ::_thesis: p `2 > ((GoB f) * (1,(width (GoB f)))) `2 then ex q being Point of (TOP-REAL 2) st ( p = q & q `2 > N-bound (L~ f) ) ; hence p `2 > ((GoB f) * (1,(width (GoB f)))) `2 by JORDAN5D:40; ::_thesis: verum end; then A3: P2 misses L~ f by GOBOARD8:24; A4: 1 + 1 <= len f by GOBOARD7:34, XXREAL_0:2; A5: ((width (GoB f)) -' 1) + 1 = width (GoB f) by GOBRD11:34, XREAL_1:235; consider i being Element of NAT such that A6: 1 <= i and A7: i < len (GoB f) and A8: N-min (L~ f) = (GoB f) * (i,(width (GoB f))) by Th28; A9: i + 1 <= len (GoB f) by A7, NAT_1:13; A10: i in dom (GoB f) by A6, A7, FINSEQ_3:25; then A11: f /. 2 = (GoB f) * ((i + 1),(width (GoB f))) by A1, A8, Th29; A12: width (GoB f) >= 1 by GOBRD11:34; then A13: [i,(width (GoB f))] in Indices (GoB f) by A6, A7, MATRIX_1:36; A14: 1 <= i + 1 by A6, NAT_1:13; then A15: (f /. 2) `2 = ((GoB f) * (1,(width (GoB f)))) `2 by A11, A12, A9, GOBOARD5:1 .= (N-min (L~ f)) `2 by A6, A7, A8, A12, GOBOARD5:1 .= N-bound (L~ f) by EUCLID:52 ; set a = ((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|; set q = (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))); A16: (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|) `2 = (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `2) + (|[0,1]| `2) by TOPREAL3:2 .= (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `2) + 1 by EUCLID:52 ; ((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `2 = ((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + (f /. 2))) `2 by A1, A8, A10, Th29 .= (1 / 2) * (((f /. 1) + (f /. 2)) `2) by A1, A8, TOPREAL3:4 .= (1 / 2) * (((f /. 1) `2) + ((f /. 2) `2)) by TOPREAL3:2 .= (1 / 2) * ((N-bound (L~ f)) + (N-bound (L~ f))) by A1, A15, EUCLID:52 .= N-bound (L~ f) ; then (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|) `2 > 0 + (N-bound (L~ f)) by A16, XREAL_1:8; then A17: (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|) `2 > N-bound (L~ (SpStSeq (L~ f))) by SPRECT_1:60; LeftComp (SpStSeq (L~ f)) = { p where p is Point of (TOP-REAL 2) : ( not W-bound (L~ (SpStSeq (L~ f))) <= p `1 or not p `1 <= E-bound (L~ (SpStSeq (L~ f))) or not S-bound (L~ (SpStSeq (L~ f))) <= p `2 or not p `2 <= N-bound (L~ (SpStSeq (L~ f))) ) } by Th37; then A18: ((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]| in LeftComp (SpStSeq (L~ f)) by A17; [(i + 1),(width (GoB f))] in Indices (GoB f) by A12, A14, A9, MATRIX_1:36; then left_cell (f,1) = cell ((GoB f),i,(width (GoB f))) by A1, A8, A11, A5, A4, A13, GOBOARD5:28; then A19: Int (cell ((GoB f),i,(width (GoB f)))) c= LeftComp f by GOBOARD9:def_1; ((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]| in Int (cell ((GoB f),i,(width (GoB f)))) by A6, A9, GOBOARD6:32; then A20: LeftComp f meets LeftComp (SpStSeq (L~ f)) by A19, A18, XBOOLE_0:3; A21: S-bound (L~ (SpStSeq (L~ f))) = S-bound (L~ f) by SPRECT_1:59; for p being Point of (TOP-REAL 2) st p in P4 holds p `1 < ((GoB f) * (1,1)) `1 proof let p be Point of (TOP-REAL 2); ::_thesis: ( p in P4 implies p `1 < ((GoB f) * (1,1)) `1 ) assume p in P4 ; ::_thesis: p `1 < ((GoB f) * (1,1)) `1 then ex q being Point of (TOP-REAL 2) st ( p = q & q `1 < W-bound (L~ f) ) ; hence p `1 < ((GoB f) * (1,1)) `1 by JORDAN5D:37; ::_thesis: verum end; then A22: P4 misses L~ f by GOBOARD8:21; for p being Point of (TOP-REAL 2) st p in P3 holds p `1 > ((GoB f) * ((len (GoB f)),1)) `1 proof let p be Point of (TOP-REAL 2); ::_thesis: ( p in P3 implies p `1 > ((GoB f) * ((len (GoB f)),1)) `1 ) assume p in P3 ; ::_thesis: p `1 > ((GoB f) * ((len (GoB f)),1)) `1 then ex q being Point of (TOP-REAL 2) st ( p = q & q `1 > E-bound (L~ f) ) ; hence p `1 > ((GoB f) * ((len (GoB f)),1)) `1 by JORDAN5D:39; ::_thesis: verum end; then P3 misses L~ f by GOBOARD8:22; then A23: P3 \/ P4 misses L~ f by A22, XBOOLE_1:70; LeftComp (SpStSeq (L~ f)) is_a_component_of (L~ (SpStSeq (L~ f))) ` by GOBOARD9:def_1; then consider B1 being Subset of ((TOP-REAL 2) | ((L~ (SpStSeq (L~ f))) `)) such that A24: B1 = LeftComp (SpStSeq (L~ f)) and A25: B1 is a_component by CONNSP_1:def_6; B1 is connected by A25, CONNSP_1:def_5; then A26: LeftComp (SpStSeq (L~ f)) is connected by A24, CONNSP_1:23; A27: E-bound (L~ (SpStSeq (L~ f))) = E-bound (L~ f) by SPRECT_1:61; A28: N-bound (L~ (SpStSeq (L~ f))) = N-bound (L~ f) by SPRECT_1:60; A29: LeftComp (SpStSeq (L~ f)) = (P1 \/ P2) \/ (P3 \/ P4) proof thus LeftComp (SpStSeq (L~ f)) c= (P1 \/ P2) \/ (P3 \/ P4) :: according to XBOOLE_0:def_10 ::_thesis: (P1 \/ P2) \/ (P3 \/ P4) c= LeftComp (SpStSeq (L~ f)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LeftComp (SpStSeq (L~ f)) or x in (P1 \/ P2) \/ (P3 \/ P4) ) assume x in LeftComp (SpStSeq (L~ f)) ; ::_thesis: x in (P1 \/ P2) \/ (P3 \/ P4) then x in { p where p is Point of (TOP-REAL 2) : ( not W-bound (L~ f) <= p `1 or not p `1 <= E-bound (L~ f) or not S-bound (L~ f) <= p `2 or not p `2 <= N-bound (L~ f) ) } by A28, A2, A21, A27, Th37; then ex p being Point of (TOP-REAL 2) st ( p = x & ( not W-bound (L~ f) <= p `1 or not p `1 <= E-bound (L~ f) or not S-bound (L~ f) <= p `2 or not p `2 <= N-bound (L~ f) ) ) ; then ( x in P1 or x in P2 or x in P3 or x in P4 ) ; then ( x in P1 \/ P2 or x in P3 \/ P4 ) by XBOOLE_0:def_3; hence x in (P1 \/ P2) \/ (P3 \/ P4) by XBOOLE_0:def_3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (P1 \/ P2) \/ (P3 \/ P4) or x in LeftComp (SpStSeq (L~ f)) ) assume x in (P1 \/ P2) \/ (P3 \/ P4) ; ::_thesis: x in LeftComp (SpStSeq (L~ f)) then A30: ( x in P1 \/ P2 or x in P3 \/ P4 ) by XBOOLE_0:def_3; percases ( x in P1 or x in P2 or x in P3 or x in P4 ) by A30, XBOOLE_0:def_3; suppose x in P1 ; ::_thesis: x in LeftComp (SpStSeq (L~ f)) then ex p being Point of (TOP-REAL 2) st ( x = p & p `2 < S-bound (L~ f) ) ; hence x in LeftComp (SpStSeq (L~ f)) by A21, Th40; ::_thesis: verum end; suppose x in P2 ; ::_thesis: x in LeftComp (SpStSeq (L~ f)) then ex p being Point of (TOP-REAL 2) st ( x = p & p `2 > N-bound (L~ f) ) ; hence x in LeftComp (SpStSeq (L~ f)) by A28, Th40; ::_thesis: verum end; suppose x in P3 ; ::_thesis: x in LeftComp (SpStSeq (L~ f)) then ex p being Point of (TOP-REAL 2) st ( x = p & p `1 > E-bound (L~ f) ) ; hence x in LeftComp (SpStSeq (L~ f)) by A27, Th40; ::_thesis: verum end; suppose x in P4 ; ::_thesis: x in LeftComp (SpStSeq (L~ f)) then ex p being Point of (TOP-REAL 2) st ( x = p & p `1 < W-bound (L~ f) ) ; hence x in LeftComp (SpStSeq (L~ f)) by A2, Th40; ::_thesis: verum end; end; end; for p being Point of (TOP-REAL 2) st p in P1 holds p `2 < ((GoB f) * (1,1)) `2 proof let p be Point of (TOP-REAL 2); ::_thesis: ( p in P1 implies p `2 < ((GoB f) * (1,1)) `2 ) assume p in P1 ; ::_thesis: p `2 < ((GoB f) * (1,1)) `2 then ex q being Point of (TOP-REAL 2) st ( p = q & q `2 < S-bound (L~ f) ) ; hence p `2 < ((GoB f) * (1,1)) `2 by JORDAN5D:38; ::_thesis: verum end; then P1 misses L~ f by GOBOARD8:23; then P1 \/ P2 misses L~ f by A3, XBOOLE_1:70; then LeftComp (SpStSeq (L~ f)) misses L~ f by A29, A23, XBOOLE_1:70; then A31: LeftComp (SpStSeq (L~ f)) c= (L~ f) ` by SUBSET_1:23; LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def_1; hence LeftComp (SpStSeq (L~ f)) c= LeftComp f by A26, A20, A31, GOBOARD9:4; ::_thesis: verum end; begin theorem Th42: :: SPRECT_3:42 for f being FinSequence of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) holds ( <*p,q*> is_in_the_area_of f iff ( <*p*> is_in_the_area_of f & <*q*> is_in_the_area_of f ) ) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p, q being Point of (TOP-REAL 2) holds ( <*p,q*> is_in_the_area_of f iff ( <*p*> is_in_the_area_of f & <*q*> is_in_the_area_of f ) ) let p, q be Point of (TOP-REAL 2); ::_thesis: ( <*p,q*> is_in_the_area_of f iff ( <*p*> is_in_the_area_of f & <*q*> is_in_the_area_of f ) ) thus ( <*p,q*> is_in_the_area_of f implies ( <*p*> is_in_the_area_of f & <*q*> is_in_the_area_of f ) ) ::_thesis: ( <*p*> is_in_the_area_of f & <*q*> is_in_the_area_of f implies <*p,q*> is_in_the_area_of f ) proof A1: dom <*p,q*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89; then A2: 1 in dom <*p,q*> by TARSKI:def_2; assume A3: <*p,q*> is_in_the_area_of f ; ::_thesis: ( <*p*> is_in_the_area_of f & <*q*> is_in_the_area_of f ) A4: <*p,q*> /. 1 = p by FINSEQ_4:17; then A5: p `1 <= E-bound (L~ f) by A3, A2, SPRECT_2:def_1; A6: p `2 <= N-bound (L~ f) by A3, A2, A4, SPRECT_2:def_1; A7: S-bound (L~ f) <= p `2 by A3, A2, A4, SPRECT_2:def_1; A8: W-bound (L~ f) <= p `1 by A3, A2, A4, SPRECT_2:def_1; thus <*p*> is_in_the_area_of f ::_thesis: <*q*> is_in_the_area_of f proof let i be Element of NAT ; :: according to SPRECT_2:def_1 ::_thesis: ( not i in dom <*p*> or ( W-bound (L~ f) <= (<*p*> /. i) `1 & (<*p*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*p*> /. i) `2 & (<*p*> /. i) `2 <= N-bound (L~ f) ) ) assume i in dom <*p*> ; ::_thesis: ( W-bound (L~ f) <= (<*p*> /. i) `1 & (<*p*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*p*> /. i) `2 & (<*p*> /. i) `2 <= N-bound (L~ f) ) then i in {1} by FINSEQ_1:2, FINSEQ_1:38; then i = 1 by TARSKI:def_1; hence ( W-bound (L~ f) <= (<*p*> /. i) `1 & (<*p*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*p*> /. i) `2 & (<*p*> /. i) `2 <= N-bound (L~ f) ) by A8, A5, A7, A6, FINSEQ_4:16; ::_thesis: verum end; let i be Element of NAT ; :: according to SPRECT_2:def_1 ::_thesis: ( not i in dom <*q*> or ( W-bound (L~ f) <= (<*q*> /. i) `1 & (<*q*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*q*> /. i) `2 & (<*q*> /. i) `2 <= N-bound (L~ f) ) ) assume i in dom <*q*> ; ::_thesis: ( W-bound (L~ f) <= (<*q*> /. i) `1 & (<*q*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*q*> /. i) `2 & (<*q*> /. i) `2 <= N-bound (L~ f) ) then i in {1} by FINSEQ_1:2, FINSEQ_1:38; then A9: i = 1 by TARSKI:def_1; A10: <*p,q*> /. 2 = q by FINSEQ_4:17; A11: 2 in dom <*p,q*> by A1, TARSKI:def_2; then A12: q `1 <= E-bound (L~ f) by A3, A10, SPRECT_2:def_1; A13: q `2 <= N-bound (L~ f) by A3, A11, A10, SPRECT_2:def_1; A14: S-bound (L~ f) <= q `2 by A3, A11, A10, SPRECT_2:def_1; W-bound (L~ f) <= q `1 by A3, A11, A10, SPRECT_2:def_1; hence ( W-bound (L~ f) <= (<*q*> /. i) `1 & (<*q*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*q*> /. i) `2 & (<*q*> /. i) `2 <= N-bound (L~ f) ) by A12, A14, A13, A9, FINSEQ_4:16; ::_thesis: verum end; A15: <*p*> /. 1 = p by FINSEQ_4:16; dom <*q*> = {1} by FINSEQ_1:2, FINSEQ_1:38; then A16: 1 in dom <*q*> by TARSKI:def_1; dom <*p*> = {1} by FINSEQ_1:2, FINSEQ_1:38; then A17: 1 in dom <*p*> by TARSKI:def_1; assume A18: <*p*> is_in_the_area_of f ; ::_thesis: ( not <*q*> is_in_the_area_of f or <*p,q*> is_in_the_area_of f ) then A19: p `1 <= E-bound (L~ f) by A17, A15, SPRECT_2:def_1; A20: p `2 <= N-bound (L~ f) by A18, A17, A15, SPRECT_2:def_1; A21: S-bound (L~ f) <= p `2 by A18, A17, A15, SPRECT_2:def_1; A22: <*q*> /. 1 = q by FINSEQ_4:16; assume A23: <*q*> is_in_the_area_of f ; ::_thesis: <*p,q*> is_in_the_area_of f then A24: W-bound (L~ f) <= q `1 by A16, A22, SPRECT_2:def_1; A25: q `1 <= E-bound (L~ f) by A23, A16, A22, SPRECT_2:def_1; let i be Element of NAT ; :: according to SPRECT_2:def_1 ::_thesis: ( not i in dom <*p,q*> or ( W-bound (L~ f) <= (<*p,q*> /. i) `1 & (<*p,q*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*p,q*> /. i) `2 & (<*p,q*> /. i) `2 <= N-bound (L~ f) ) ) assume i in dom <*p,q*> ; ::_thesis: ( W-bound (L~ f) <= (<*p,q*> /. i) `1 & (<*p,q*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*p,q*> /. i) `2 & (<*p,q*> /. i) `2 <= N-bound (L~ f) ) then i in {1,2} by FINSEQ_1:2, FINSEQ_1:89; then A26: ( i = 1 or i = 2 ) by TARSKI:def_2; A27: q `2 <= N-bound (L~ f) by A23, A16, A22, SPRECT_2:def_1; A28: S-bound (L~ f) <= q `2 by A23, A16, A22, SPRECT_2:def_1; W-bound (L~ f) <= p `1 by A18, A17, A15, SPRECT_2:def_1; hence ( W-bound (L~ f) <= (<*p,q*> /. i) `1 & (<*p,q*> /. i) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*p,q*> /. i) `2 & (<*p,q*> /. i) `2 <= N-bound (L~ f) ) by A19, A21, A20, A24, A25, A28, A27, A26, FINSEQ_4:17; ::_thesis: verum end; theorem Th43: :: SPRECT_3:43 for f being rectangular FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st <*p*> is_in_the_area_of f & ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) ) holds p in L~ f proof let f be rectangular FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st <*p*> is_in_the_area_of f & ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) ) holds p in L~ f let p be Point of (TOP-REAL 2); ::_thesis: ( <*p*> is_in_the_area_of f & ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) ) implies p in L~ f ) A1: <*p*> /. 1 = p by FINSEQ_4:16; dom <*p*> = {1} by FINSEQ_1:2, FINSEQ_1:38; then A2: 1 in dom <*p*> by TARSKI:def_1; assume A3: <*p*> is_in_the_area_of f ; ::_thesis: ( ( not p `1 = W-bound (L~ f) & not p `1 = E-bound (L~ f) & not p `2 = S-bound (L~ f) & not p `2 = N-bound (L~ f) ) or p in L~ f ) then A4: W-bound (L~ f) <= p `1 by A2, A1, SPRECT_2:def_1; A5: p `2 <= N-bound (L~ f) by A3, A2, A1, SPRECT_2:def_1; A6: S-bound (L~ f) <= p `2 by A3, A2, A1, SPRECT_2:def_1; A7: p `1 <= E-bound (L~ f) by A3, A2, A1, SPRECT_2:def_1; consider D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) such that A8: f = SpStSeq D by SPRECT_1:def_2; A9: E-bound (L~ (SpStSeq D)) = E-bound D by SPRECT_1:61; A10: N-bound (L~ (SpStSeq D)) = N-bound D by SPRECT_1:60; A11: S-bound (L~ (SpStSeq D)) = S-bound D by SPRECT_1:59; A12: W-bound (L~ (SpStSeq D)) = W-bound D by SPRECT_1:58; A13: L~ f = ((LSeg ((NW-corner D),(NE-corner D))) \/ (LSeg ((NE-corner D),(SE-corner D)))) \/ ((LSeg ((SE-corner D),(SW-corner D))) \/ (LSeg ((SW-corner D),(NW-corner D)))) by A8, SPRECT_1:41; assume A14: ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) ) ; ::_thesis: p in L~ f percases ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) ) by A14; supposeA15: p `1 = W-bound (L~ f) ; ::_thesis: p in L~ f A16: (NW-corner D) `1 = W-bound D by EUCLID:52; A17: (NW-corner D) `2 = N-bound D by EUCLID:52; A18: (SW-corner D) `2 = S-bound D by EUCLID:52; (SW-corner D) `1 = W-bound D by EUCLID:52; then p in LSeg ((SW-corner D),(NW-corner D)) by A6, A5, A8, A12, A11, A10, A15, A16, A18, A17, GOBOARD7:7; then p in (LSeg ((SE-corner D),(SW-corner D))) \/ (LSeg ((SW-corner D),(NW-corner D))) by XBOOLE_0:def_3; hence p in L~ f by A13, XBOOLE_0:def_3; ::_thesis: verum end; supposeA19: p `1 = E-bound (L~ f) ; ::_thesis: p in L~ f A20: (SE-corner D) `1 = E-bound D by EUCLID:52; A21: (SE-corner D) `2 = S-bound D by EUCLID:52; A22: (NE-corner D) `2 = N-bound D by EUCLID:52; (NE-corner D) `1 = E-bound D by EUCLID:52; then p in LSeg ((NE-corner D),(SE-corner D)) by A6, A5, A8, A11, A10, A9, A19, A20, A22, A21, GOBOARD7:7; then p in (LSeg ((NW-corner D),(NE-corner D))) \/ (LSeg ((NE-corner D),(SE-corner D))) by XBOOLE_0:def_3; hence p in L~ f by A13, XBOOLE_0:def_3; ::_thesis: verum end; supposeA23: p `2 = S-bound (L~ f) ; ::_thesis: p in L~ f A24: (SW-corner D) `1 = W-bound D by EUCLID:52; A25: (SW-corner D) `2 = S-bound D by EUCLID:52; A26: (SE-corner D) `2 = S-bound D by EUCLID:52; (SE-corner D) `1 = E-bound D by EUCLID:52; then p in LSeg ((SE-corner D),(SW-corner D)) by A4, A7, A8, A12, A11, A9, A23, A24, A26, A25, GOBOARD7:8; then p in (LSeg ((SE-corner D),(SW-corner D))) \/ (LSeg ((SW-corner D),(NW-corner D))) by XBOOLE_0:def_3; hence p in L~ f by A13, XBOOLE_0:def_3; ::_thesis: verum end; supposeA27: p `2 = N-bound (L~ f) ; ::_thesis: p in L~ f A28: (NE-corner D) `1 = E-bound D by EUCLID:52; A29: (NE-corner D) `2 = N-bound D by EUCLID:52; A30: (NW-corner D) `2 = N-bound D by EUCLID:52; (NW-corner D) `1 = W-bound D by EUCLID:52; then p in LSeg ((NW-corner D),(NE-corner D)) by A4, A7, A8, A12, A10, A9, A27, A28, A30, A29, GOBOARD7:8; then p in (LSeg ((NW-corner D),(NE-corner D))) \/ (LSeg ((NE-corner D),(SE-corner D))) by XBOOLE_0:def_3; hence p in L~ f by A13, XBOOLE_0:def_3; ::_thesis: verum end; end; end; theorem Th44: :: SPRECT_3:44 for f being FinSequence of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) for r being Real st 0 <= r & r <= 1 & <*p,q*> is_in_the_area_of f holds <*(((1 - r) * p) + (r * q))*> is_in_the_area_of f proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p, q being Point of (TOP-REAL 2) for r being Real st 0 <= r & r <= 1 & <*p,q*> is_in_the_area_of f holds <*(((1 - r) * p) + (r * q))*> is_in_the_area_of f let p, q be Point of (TOP-REAL 2); ::_thesis: for r being Real st 0 <= r & r <= 1 & <*p,q*> is_in_the_area_of f holds <*(((1 - r) * p) + (r * q))*> is_in_the_area_of f let r be Real; ::_thesis: ( 0 <= r & r <= 1 & <*p,q*> is_in_the_area_of f implies <*(((1 - r) * p) + (r * q))*> is_in_the_area_of f ) assume that A1: 0 <= r and A2: r <= 1 and A3: <*p,q*> is_in_the_area_of f ; ::_thesis: <*(((1 - r) * p) + (r * q))*> is_in_the_area_of f A4: dom <*p,q*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89; then A5: 2 in dom <*p,q*> by TARSKI:def_2; A6: <*p,q*> /. 2 = q by FINSEQ_4:17; then W-bound (L~ f) <= q `1 by A3, A5, SPRECT_2:def_1; then A7: r * (W-bound (L~ f)) <= r * (q `1) by A1, XREAL_1:64; q `1 <= E-bound (L~ f) by A3, A5, A6, SPRECT_2:def_1; then A8: r * (q `1) <= r * (E-bound (L~ f)) by A1, XREAL_1:64; A9: <*p,q*> /. 1 = p by FINSEQ_4:17; A10: 1 - r >= 0 by A2, XREAL_1:48; A11: 1 in dom <*p,q*> by A4, TARSKI:def_2; then W-bound (L~ f) <= p `1 by A3, A9, SPRECT_2:def_1; then A12: (1 - r) * (W-bound (L~ f)) <= (1 - r) * (p `1) by A10, XREAL_1:64; p `1 <= E-bound (L~ f) by A3, A11, A9, SPRECT_2:def_1; then A13: (1 - r) * (p `1) <= (1 - r) * (E-bound (L~ f)) by A10, XREAL_1:64; S-bound (L~ f) <= p `2 by A3, A11, A9, SPRECT_2:def_1; then A14: (1 - r) * (S-bound (L~ f)) <= (1 - r) * (p `2) by A10, XREAL_1:64; A15: (((1 - r) * p) + (r * q)) `1 = (((1 - r) * p) `1) + ((r * q) `1) by TOPREAL3:2 .= ((1 - r) * (p `1)) + ((r * q) `1) by TOPREAL3:4 .= ((1 - r) * (p `1)) + (r * (q `1)) by TOPREAL3:4 ; p `2 <= N-bound (L~ f) by A3, A11, A9, SPRECT_2:def_1; then A16: (1 - r) * (p `2) <= (1 - r) * (N-bound (L~ f)) by A10, XREAL_1:64; let n be Element of NAT ; :: according to SPRECT_2:def_1 ::_thesis: ( not n in dom <*(((1 - r) * p) + (r * q))*> or ( W-bound (L~ f) <= (<*(((1 - r) * p) + (r * q))*> /. n) `1 & (<*(((1 - r) * p) + (r * q))*> /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*(((1 - r) * p) + (r * q))*> /. n) `2 & (<*(((1 - r) * p) + (r * q))*> /. n) `2 <= N-bound (L~ f) ) ) A17: dom <*(((1 - r) * p) + (r * q))*> = {1} by FINSEQ_1:2, FINSEQ_1:38; assume n in dom <*(((1 - r) * p) + (r * q))*> ; ::_thesis: ( W-bound (L~ f) <= (<*(((1 - r) * p) + (r * q))*> /. n) `1 & (<*(((1 - r) * p) + (r * q))*> /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*(((1 - r) * p) + (r * q))*> /. n) `2 & (<*(((1 - r) * p) + (r * q))*> /. n) `2 <= N-bound (L~ f) ) then A18: n = 1 by A17, TARSKI:def_1; ((1 - r) * (W-bound (L~ f))) + (r * (W-bound (L~ f))) = 1 * (W-bound (L~ f)) ; then W-bound (L~ f) <= ((1 - r) * (p `1)) + (r * (q `1)) by A7, A12, XREAL_1:7; hence W-bound (L~ f) <= (<*(((1 - r) * p) + (r * q))*> /. n) `1 by A18, A15, FINSEQ_4:16; ::_thesis: ( (<*(((1 - r) * p) + (r * q))*> /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*(((1 - r) * p) + (r * q))*> /. n) `2 & (<*(((1 - r) * p) + (r * q))*> /. n) `2 <= N-bound (L~ f) ) ((1 - r) * (E-bound (L~ f))) + (r * (E-bound (L~ f))) = 1 * (E-bound (L~ f)) ; then ((1 - r) * (p `1)) + (r * (q `1)) <= E-bound (L~ f) by A8, A13, XREAL_1:7; hence (<*(((1 - r) * p) + (r * q))*> /. n) `1 <= E-bound (L~ f) by A18, A15, FINSEQ_4:16; ::_thesis: ( S-bound (L~ f) <= (<*(((1 - r) * p) + (r * q))*> /. n) `2 & (<*(((1 - r) * p) + (r * q))*> /. n) `2 <= N-bound (L~ f) ) A19: (((1 - r) * p) + (r * q)) `2 = (((1 - r) * p) `2) + ((r * q) `2) by TOPREAL3:2 .= ((1 - r) * (p `2)) + ((r * q) `2) by TOPREAL3:4 .= ((1 - r) * (p `2)) + (r * (q `2)) by TOPREAL3:4 ; q `2 <= N-bound (L~ f) by A3, A5, A6, SPRECT_2:def_1; then A20: r * (q `2) <= r * (N-bound (L~ f)) by A1, XREAL_1:64; S-bound (L~ f) <= q `2 by A3, A5, A6, SPRECT_2:def_1; then A21: r * (S-bound (L~ f)) <= r * (q `2) by A1, XREAL_1:64; ((1 - r) * (S-bound (L~ f))) + (r * (S-bound (L~ f))) = 1 * (S-bound (L~ f)) ; then S-bound (L~ f) <= ((1 - r) * (p `2)) + (r * (q `2)) by A21, A14, XREAL_1:7; hence S-bound (L~ f) <= (<*(((1 - r) * p) + (r * q))*> /. n) `2 by A18, A19, FINSEQ_4:16; ::_thesis: (<*(((1 - r) * p) + (r * q))*> /. n) `2 <= N-bound (L~ f) ((1 - r) * (N-bound (L~ f))) + (r * (N-bound (L~ f))) = 1 * (N-bound (L~ f)) ; then ((1 - r) * (p `2)) + (r * (q `2)) <= N-bound (L~ f) by A20, A16, XREAL_1:7; hence (<*(((1 - r) * p) + (r * q))*> /. n) `2 <= N-bound (L~ f) by A18, A19, FINSEQ_4:16; ::_thesis: verum end; theorem Th45: :: SPRECT_3:45 for i being Element of NAT for f, g being FinSequence of (TOP-REAL 2) st g is_in_the_area_of f & i in dom g holds <*(g /. i)*> is_in_the_area_of f proof let i be Element of NAT ; ::_thesis: for f, g being FinSequence of (TOP-REAL 2) st g is_in_the_area_of f & i in dom g holds <*(g /. i)*> is_in_the_area_of f let f, g be FinSequence of (TOP-REAL 2); ::_thesis: ( g is_in_the_area_of f & i in dom g implies <*(g /. i)*> is_in_the_area_of f ) assume that A1: g is_in_the_area_of f and A2: i in dom g ; ::_thesis: <*(g /. i)*> is_in_the_area_of f let n be Element of NAT ; :: according to SPRECT_2:def_1 ::_thesis: ( not n in dom <*(g /. i)*> or ( W-bound (L~ f) <= (<*(g /. i)*> /. n) `1 & (<*(g /. i)*> /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*(g /. i)*> /. n) `2 & (<*(g /. i)*> /. n) `2 <= N-bound (L~ f) ) ) A3: dom <*(g /. i)*> = {1} by FINSEQ_1:2, FINSEQ_1:38; assume n in dom <*(g /. i)*> ; ::_thesis: ( W-bound (L~ f) <= (<*(g /. i)*> /. n) `1 & (<*(g /. i)*> /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*(g /. i)*> /. n) `2 & (<*(g /. i)*> /. n) `2 <= N-bound (L~ f) ) then n = 1 by A3, TARSKI:def_1; then <*(g /. i)*> /. n = g /. i by FINSEQ_4:16; hence ( W-bound (L~ f) <= (<*(g /. i)*> /. n) `1 & (<*(g /. i)*> /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*(g /. i)*> /. n) `2 & (<*(g /. i)*> /. n) `2 <= N-bound (L~ f) ) by A1, A2, SPRECT_2:def_1; ::_thesis: verum end; theorem Th46: :: SPRECT_3:46 for f, g being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st g is_in_the_area_of f & p in L~ g holds <*p*> is_in_the_area_of f proof let f, g be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st g is_in_the_area_of f & p in L~ g holds <*p*> is_in_the_area_of f let p be Point of (TOP-REAL 2); ::_thesis: ( g is_in_the_area_of f & p in L~ g implies <*p*> is_in_the_area_of f ) assume A1: g is_in_the_area_of f ; ::_thesis: ( not p in L~ g or <*p*> is_in_the_area_of f ) assume p in L~ g ; ::_thesis: <*p*> is_in_the_area_of f then consider i being Element of NAT such that A2: 1 <= i and A3: i + 1 <= len g and A4: p in LSeg ((g /. i),(g /. (i + 1))) by SPPOL_2:14; A5: ex r being Real st ( p = ((1 - r) * (g /. i)) + (r * (g /. (i + 1))) & 0 <= r & r <= 1 ) by A4; i <= i + 1 by NAT_1:11; then i <= len g by A3, XXREAL_0:2; then i in dom g by A2, FINSEQ_3:25; then A6: <*(g /. i)*> is_in_the_area_of f by A1, Th45; 1 <= i + 1 by NAT_1:11; then i + 1 in dom g by A3, FINSEQ_3:25; then <*(g /. (i + 1))*> is_in_the_area_of f by A1, Th45; then <*(g /. i),(g /. (i + 1))*> is_in_the_area_of f by A6, Th42; hence <*p*> is_in_the_area_of f by A5, Th44; ::_thesis: verum end; theorem Th47: :: SPRECT_3:47 for f being rectangular FinSequence of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) st not q in L~ f & <*p,q*> is_in_the_area_of f holds (LSeg (p,q)) /\ (L~ f) c= {p} proof let f be rectangular FinSequence of (TOP-REAL 2); ::_thesis: for p, q being Point of (TOP-REAL 2) st not q in L~ f & <*p,q*> is_in_the_area_of f holds (LSeg (p,q)) /\ (L~ f) c= {p} let p, q be Point of (TOP-REAL 2); ::_thesis: ( not q in L~ f & <*p,q*> is_in_the_area_of f implies (LSeg (p,q)) /\ (L~ f) c= {p} ) assume A1: not q in L~ f ; ::_thesis: ( not <*p,q*> is_in_the_area_of f or (LSeg (p,q)) /\ (L~ f) c= {p} ) assume A2: <*p,q*> is_in_the_area_of f ; ::_thesis: (LSeg (p,q)) /\ (L~ f) c= {p} A3: dom <*p,q*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89; then A4: 2 in dom <*p,q*> by TARSKI:def_2; A5: <*p,q*> /. 2 = q by FINSEQ_4:17; then A6: W-bound (L~ f) <= q `1 by A2, A4, SPRECT_2:def_1; A7: <*q*> is_in_the_area_of f by A2, Th42; then q `1 <> W-bound (L~ f) by A1, Th43; then A8: W-bound (L~ f) < q `1 by A6, XXREAL_0:1; A9: q `2 <= N-bound (L~ f) by A2, A4, A5, SPRECT_2:def_1; q `2 <> N-bound (L~ f) by A1, A7, Th43; then A10: q `2 < N-bound (L~ f) by A9, XXREAL_0:1; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (LSeg (p,q)) /\ (L~ f) or x in {p} ) A11: <*p,q*> /. 1 = p by FINSEQ_4:17; A12: q `1 <= E-bound (L~ f) by A2, A4, A5, SPRECT_2:def_1; q `1 <> E-bound (L~ f) by A1, A7, Th43; then A13: q `1 < E-bound (L~ f) by A12, XXREAL_0:1; assume A14: x in (LSeg (p,q)) /\ (L~ f) ; ::_thesis: x in {p} then reconsider p9 = x as Point of (TOP-REAL 2) ; A15: p9 in L~ f by A14, XBOOLE_0:def_4; A16: 1 in dom <*p,q*> by A3, TARSKI:def_2; then A17: W-bound (L~ f) <= p `1 by A2, A11, SPRECT_2:def_1; A18: p `2 <= N-bound (L~ f) by A2, A16, A11, SPRECT_2:def_1; A19: S-bound (L~ f) <= p `2 by A2, A16, A11, SPRECT_2:def_1; A20: p `1 <= E-bound (L~ f) by A2, A16, A11, SPRECT_2:def_1; A21: S-bound (L~ f) <= q `2 by A2, A4, A5, SPRECT_2:def_1; q `2 <> S-bound (L~ f) by A1, A7, Th43; then A22: S-bound (L~ f) < q `2 by A21, XXREAL_0:1; x in LSeg (p,q) by A14, XBOOLE_0:def_4; then consider r being Real such that A23: p9 = ((1 - r) * p) + (r * q) and A24: 0 <= r and A25: r <= 1 ; A26: p9 `1 = (((1 - r) * p) `1) + ((r * q) `1) by A23, TOPREAL3:2 .= ((1 - r) * (p `1)) + ((r * q) `1) by TOPREAL3:4 .= ((1 - r) * (p `1)) + (r * (q `1)) by TOPREAL3:4 ; A27: p9 `2 = (((1 - r) * p) `2) + ((r * q) `2) by A23, TOPREAL3:2 .= ((1 - r) * (p `2)) + ((r * q) `2) by TOPREAL3:4 .= ((1 - r) * (p `2)) + (r * (q `2)) by TOPREAL3:4 ; percases ( p9 `1 = W-bound (L~ f) or p9 `1 = E-bound (L~ f) or p9 `2 = S-bound (L~ f) or p9 `2 = N-bound (L~ f) ) by A15, Th32; suppose p9 `1 = W-bound (L~ f) ; ::_thesis: x in {p} then r = 0 by A17, A8, A24, A25, A26, XREAL_1:180; then p9 = (1 * p) + (0. (TOP-REAL 2)) by A23, EUCLID:29 .= 1 * p by EUCLID:27 .= p by EUCLID:29 ; hence x in {p} by ZFMISC_1:31; ::_thesis: verum end; suppose p9 `1 = E-bound (L~ f) ; ::_thesis: x in {p} then r = 0 by A20, A13, A24, A25, A26, XREAL_1:179; then p9 = (1 * p) + (0. (TOP-REAL 2)) by A23, EUCLID:29 .= 1 * p by EUCLID:27 .= p by EUCLID:29 ; hence x in {p} by ZFMISC_1:31; ::_thesis: verum end; suppose p9 `2 = S-bound (L~ f) ; ::_thesis: x in {p} then r = 0 by A19, A22, A24, A25, A27, XREAL_1:180; then p9 = (1 * p) + (0. (TOP-REAL 2)) by A23, EUCLID:29 .= 1 * p by EUCLID:27 .= p by EUCLID:29 ; hence x in {p} by ZFMISC_1:31; ::_thesis: verum end; suppose p9 `2 = N-bound (L~ f) ; ::_thesis: x in {p} then r = 0 by A18, A10, A24, A25, A27, XREAL_1:179; then p9 = (1 * p) + (0. (TOP-REAL 2)) by A23, EUCLID:29 .= 1 * p by EUCLID:27 .= p by EUCLID:29 ; hence x in {p} by ZFMISC_1:31; ::_thesis: verum end; end; end; theorem :: SPRECT_3:48 for f being rectangular FinSequence of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) st p in L~ f & not q in L~ f & <*q*> is_in_the_area_of f holds (LSeg (p,q)) /\ (L~ f) = {p} proof let f be rectangular FinSequence of (TOP-REAL 2); ::_thesis: for p, q being Point of (TOP-REAL 2) st p in L~ f & not q in L~ f & <*q*> is_in_the_area_of f holds (LSeg (p,q)) /\ (L~ f) = {p} let p, q be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f & not q in L~ f & <*q*> is_in_the_area_of f implies (LSeg (p,q)) /\ (L~ f) = {p} ) assume that A1: p in L~ f and A2: not q in L~ f and A3: <*q*> is_in_the_area_of f ; ::_thesis: (LSeg (p,q)) /\ (L~ f) = {p} A4: <*p,q*> = <*p*> ^ <*q*> by FINSEQ_1:def_9; <*p*> is_in_the_area_of f by A1, Th46, SPRECT_2:21; hence (LSeg (p,q)) /\ (L~ f) c= {p} by A2, A3, A4, Th47, SPRECT_2:24; :: according to XBOOLE_0:def_10 ::_thesis: {p} c= (LSeg (p,q)) /\ (L~ f) p in LSeg (p,q) by RLTOPSP1:68; then p in (LSeg (p,q)) /\ (L~ f) by A1, XBOOLE_0:def_4; hence {p} c= (LSeg (p,q)) /\ (L~ f) by ZFMISC_1:31; ::_thesis: verum end; theorem Th49: :: SPRECT_3:49 for i, j being Element of NAT for f being non constant standard special_circular_sequence st 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) holds <*((GoB f) * (i,j))*> is_in_the_area_of f proof let i, j be Element of NAT ; ::_thesis: for f being non constant standard special_circular_sequence st 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) holds <*((GoB f) * (i,j))*> is_in_the_area_of f let f be non constant standard special_circular_sequence; ::_thesis: ( 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) implies <*((GoB f) * (i,j))*> is_in_the_area_of f ) assume that A1: 1 <= i and A2: i <= len (GoB f) and A3: 1 <= j and A4: j <= width (GoB f) ; ::_thesis: <*((GoB f) * (i,j))*> is_in_the_area_of f set G = GoB f; A5: 1 <= width (GoB f) by A3, A4, XXREAL_0:2; A6: 1 <= len (GoB f) by A1, A2, XXREAL_0:2; A7: N-bound (L~ f) = ((GoB f) * (1,(width (GoB f)))) `2 by JORDAN5D:40 .= ((GoB f) * (i,(width (GoB f)))) `2 by A1, A2, A5, GOBOARD5:1 ; A8: ( j = 1 or j > 1 ) by A3, XXREAL_0:1; A9: S-bound (L~ f) = ((GoB f) * (1,1)) `2 by JORDAN5D:38 .= ((GoB f) * (i,1)) `2 by A1, A2, A5, GOBOARD5:1 ; A10: ( i = 1 or i > 1 ) by A1, XXREAL_0:1; A11: E-bound (L~ f) = ((GoB f) * ((len (GoB f)),1)) `1 by JORDAN5D:39 .= ((GoB f) * ((len (GoB f)),j)) `1 by A3, A4, A6, GOBOARD5:2 ; A12: ( j = width (GoB f) or j < width (GoB f) ) by A4, XXREAL_0:1; A13: ( i = len (GoB f) or i < len (GoB f) ) by A2, XXREAL_0:1; let n be Element of NAT ; :: according to SPRECT_2:def_1 ::_thesis: ( not n in dom <*((GoB f) * (i,j))*> or ( W-bound (L~ f) <= (<*((GoB f) * (i,j))*> /. n) `1 & (<*((GoB f) * (i,j))*> /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*((GoB f) * (i,j))*> /. n) `2 & (<*((GoB f) * (i,j))*> /. n) `2 <= N-bound (L~ f) ) ) set p = (GoB f) * (i,j); assume n in dom <*((GoB f) * (i,j))*> ; ::_thesis: ( W-bound (L~ f) <= (<*((GoB f) * (i,j))*> /. n) `1 & (<*((GoB f) * (i,j))*> /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*((GoB f) * (i,j))*> /. n) `2 & (<*((GoB f) * (i,j))*> /. n) `2 <= N-bound (L~ f) ) then n in {1} by FINSEQ_1:2, FINSEQ_1:38; then n = 1 by TARSKI:def_1; then A14: <*((GoB f) * (i,j))*> /. n = (GoB f) * (i,j) by FINSEQ_4:16; W-bound (L~ f) = ((GoB f) * (1,1)) `1 by JORDAN5D:37 .= ((GoB f) * (1,j)) `1 by A3, A4, A6, GOBOARD5:2 ; hence ( W-bound (L~ f) <= (<*((GoB f) * (i,j))*> /. n) `1 & (<*((GoB f) * (i,j))*> /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*((GoB f) * (i,j))*> /. n) `2 & (<*((GoB f) * (i,j))*> /. n) `2 <= N-bound (L~ f) ) by A14, A10, A9, A8, A11, A13, A7, A12, GOBOARD5:3, GOBOARD5:4; ::_thesis: verum end; theorem :: SPRECT_3:50 for g being FinSequence of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) st <*p,q*> is_in_the_area_of g holds <*((1 / 2) * (p + q))*> is_in_the_area_of g proof let g be FinSequence of (TOP-REAL 2); ::_thesis: for p, q being Point of (TOP-REAL 2) st <*p,q*> is_in_the_area_of g holds <*((1 / 2) * (p + q))*> is_in_the_area_of g let p, q be Point of (TOP-REAL 2); ::_thesis: ( <*p,q*> is_in_the_area_of g implies <*((1 / 2) * (p + q))*> is_in_the_area_of g ) (1 / 2) * (p + q) = ((1 - (1 / 2)) * p) + ((1 / 2) * q) by EUCLID:32; hence ( <*p,q*> is_in_the_area_of g implies <*((1 / 2) * (p + q))*> is_in_the_area_of g ) by Th44; ::_thesis: verum end; theorem :: SPRECT_3:51 for f, g being FinSequence of (TOP-REAL 2) st g is_in_the_area_of f holds Rev g is_in_the_area_of f proof let f, g be FinSequence of (TOP-REAL 2); ::_thesis: ( g is_in_the_area_of f implies Rev g is_in_the_area_of f ) assume A1: g is_in_the_area_of f ; ::_thesis: Rev g is_in_the_area_of f A2: Rev (Rev g) = g ; let n be Element of NAT ; :: according to SPRECT_2:def_1 ::_thesis: ( not n in dom (Rev g) or ( W-bound (L~ f) <= ((Rev g) /. n) `1 & ((Rev g) /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= ((Rev g) /. n) `2 & ((Rev g) /. n) `2 <= N-bound (L~ f) ) ) assume A3: n in dom (Rev g) ; ::_thesis: ( W-bound (L~ f) <= ((Rev g) /. n) `1 & ((Rev g) /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= ((Rev g) /. n) `2 & ((Rev g) /. n) `2 <= N-bound (L~ f) ) n >= 1 by A3, FINSEQ_3:25; then A4: n - 1 >= 0 by XREAL_1:48; set i = ((len g) + 1) -' n; A5: len (Rev g) = len g by FINSEQ_5:def_3; then A6: n <= len g by A3, FINSEQ_3:25; then A7: ((len g) + 1) -' n = ((len g) -' n) + 1 by NAT_D:38; then ((len g) + 1) -' n = ((len g) - n) + 1 by A6, XREAL_1:233 .= (len g) - (n - 1) ; then A8: ((len g) + 1) -' n <= (len g) - 0 by A4, XREAL_1:13; 1 <= ((len g) + 1) -' n by A7, NAT_1:11; then A9: ((len g) + 1) -' n in dom g by A8, FINSEQ_3:25; len g <= (len g) + 1 by NAT_1:11; then n + (((len g) + 1) -' n) = (len g) + 1 by A6, XREAL_1:235, XXREAL_0:2; then (Rev g) /. n = g /. (((len g) + 1) -' n) by A2, A5, A3, FINSEQ_5:66; hence ( W-bound (L~ f) <= ((Rev g) /. n) `1 & ((Rev g) /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= ((Rev g) /. n) `2 & ((Rev g) /. n) `2 <= N-bound (L~ f) ) by A1, A9, SPRECT_2:def_1; ::_thesis: verum end; theorem :: SPRECT_3:52 for f, g being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st g is_in_the_area_of f & <*p*> is_in_the_area_of f & g is being_S-Seq & p in L~ g holds R_Cut (g,p) is_in_the_area_of f proof let f, g be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st g is_in_the_area_of f & <*p*> is_in_the_area_of f & g is being_S-Seq & p in L~ g holds R_Cut (g,p) is_in_the_area_of f let p be Point of (TOP-REAL 2); ::_thesis: ( g is_in_the_area_of f & <*p*> is_in_the_area_of f & g is being_S-Seq & p in L~ g implies R_Cut (g,p) is_in_the_area_of f ) assume that A1: g is_in_the_area_of f and A2: <*p*> is_in_the_area_of f and A3: g is being_S-Seq ; ::_thesis: ( not p in L~ g or R_Cut (g,p) is_in_the_area_of f ) 2 <= len g by A3, TOPREAL1:def_8; then A4: 1 <= len g by XXREAL_0:2; then A5: 1 in dom g by FINSEQ_3:25; assume A6: p in L~ g ; ::_thesis: R_Cut (g,p) is_in_the_area_of f then A7: Index (p,g) < len g by JORDAN3:8; 1 <= Index (p,g) by A6, JORDAN3:8; then A8: Index (p,g) in dom g by A7, FINSEQ_3:25; percases ( p <> g . 1 or p = g . 1 ) ; suppose p <> g . 1 ; ::_thesis: R_Cut (g,p) is_in_the_area_of f then A9: R_Cut (g,p) = (mid (g,1,(Index (p,g)))) ^ <*p*> by JORDAN3:def_4; mid (g,1,(Index (p,g))) is_in_the_area_of f by A1, A5, A8, SPRECT_2:22; hence R_Cut (g,p) is_in_the_area_of f by A2, A9, SPRECT_2:24; ::_thesis: verum end; suppose p = g . 1 ; ::_thesis: R_Cut (g,p) is_in_the_area_of f then R_Cut (g,p) = <*(g . 1)*> by JORDAN3:def_4 .= <*(g /. 1)*> by A5, PARTFUN1:def_6 .= mid (g,1,1) by A4, JORDAN4:15 ; hence R_Cut (g,p) is_in_the_area_of f by A1, A5, SPRECT_2:22; ::_thesis: verum end; end; end; theorem :: SPRECT_3:53 for f being non constant standard special_circular_sequence for g being FinSequence of (TOP-REAL 2) holds ( g is_in_the_area_of f iff g is_in_the_area_of SpStSeq (L~ f) ) proof let f be non constant standard special_circular_sequence; ::_thesis: for g being FinSequence of (TOP-REAL 2) holds ( g is_in_the_area_of f iff g is_in_the_area_of SpStSeq (L~ f) ) let g be FinSequence of (TOP-REAL 2); ::_thesis: ( g is_in_the_area_of f iff g is_in_the_area_of SpStSeq (L~ f) ) A1: S-bound (L~ (SpStSeq (L~ f))) = S-bound (L~ f) by SPRECT_1:59; A2: N-bound (L~ (SpStSeq (L~ f))) = N-bound (L~ f) by SPRECT_1:60; A3: E-bound (L~ (SpStSeq (L~ f))) = E-bound (L~ f) by SPRECT_1:61; A4: W-bound (L~ (SpStSeq (L~ f))) = W-bound (L~ f) by SPRECT_1:58; thus ( g is_in_the_area_of f implies g is_in_the_area_of SpStSeq (L~ f) ) ::_thesis: ( g is_in_the_area_of SpStSeq (L~ f) implies g is_in_the_area_of f ) proof assume A5: g is_in_the_area_of f ; ::_thesis: g is_in_the_area_of SpStSeq (L~ f) let n be Element of NAT ; :: according to SPRECT_2:def_1 ::_thesis: ( not n in dom g or ( W-bound (L~ (SpStSeq (L~ f))) <= (g /. n) `1 & (g /. n) `1 <= E-bound (L~ (SpStSeq (L~ f))) & S-bound (L~ (SpStSeq (L~ f))) <= (g /. n) `2 & (g /. n) `2 <= N-bound (L~ (SpStSeq (L~ f))) ) ) thus ( not n in dom g or ( W-bound (L~ (SpStSeq (L~ f))) <= (g /. n) `1 & (g /. n) `1 <= E-bound (L~ (SpStSeq (L~ f))) & S-bound (L~ (SpStSeq (L~ f))) <= (g /. n) `2 & (g /. n) `2 <= N-bound (L~ (SpStSeq (L~ f))) ) ) by A4, A1, A2, A3, A5, SPRECT_2:def_1; ::_thesis: verum end; assume A6: g is_in_the_area_of SpStSeq (L~ f) ; ::_thesis: g is_in_the_area_of f let n be Element of NAT ; :: according to SPRECT_2:def_1 ::_thesis: ( not n in dom g or ( W-bound (L~ f) <= (g /. n) `1 & (g /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (g /. n) `2 & (g /. n) `2 <= N-bound (L~ f) ) ) thus ( not n in dom g or ( W-bound (L~ f) <= (g /. n) `1 & (g /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (g /. n) `2 & (g /. n) `2 <= N-bound (L~ f) ) ) by A4, A1, A2, A3, A6, SPRECT_2:def_1; ::_thesis: verum end; theorem :: SPRECT_3:54 for f being rectangular special_circular_sequence for g being S-Sequence_in_R2 st g /. 1 in LeftComp f & g /. (len g) in RightComp f holds L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))) is_in_the_area_of f proof let f be rectangular special_circular_sequence; ::_thesis: for g being S-Sequence_in_R2 st g /. 1 in LeftComp f & g /. (len g) in RightComp f holds L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))) is_in_the_area_of f let g be S-Sequence_in_R2; ::_thesis: ( g /. 1 in LeftComp f & g /. (len g) in RightComp f implies L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))) is_in_the_area_of f ) assume that A1: g /. 1 in LeftComp f and A2: g /. (len g) in RightComp f ; ::_thesis: L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))) is_in_the_area_of f A3: L~ g meets L~ f by A1, A2, Th33; 1 in dom g by FINSEQ_5:6; then A4: len g >= 1 by FINSEQ_3:25; set lp = Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)); set ilp = Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g); set h = L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))); L~ g is_an_arc_of g /. 1,g /. (len g) by TOPREAL1:25; then A5: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) in (L~ g) /\ (L~ f) by A3, JORDAN5C:def_2; then A6: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) in L~ g by XBOOLE_0:def_4; then A7: 1 <= Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g) by JORDAN3:8; A8: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) in LSeg (g,(Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g))) by A6, JORDAN3:9; A9: Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g) < len g by A6, JORDAN3:8; then A10: (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 <= len g by NAT_1:13; given n being Element of NAT such that A11: n in dom (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) and A12: ( W-bound (L~ f) > ((L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) /. n) `1 or ((L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) /. n) `1 > E-bound (L~ f) or S-bound (L~ f) > ((L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) /. n) `2 or ((L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) /. n) `2 > N-bound (L~ f) ) ; :: according to SPRECT_2:def_1 ::_thesis: contradiction A13: 1 <= n by A11, FINSEQ_3:25; then A14: ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 = (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + (n -' 1) by NAT_D:38; LeftComp f = { p where p is Point of (TOP-REAL 2) : ( not W-bound (L~ f) <= p `1 or not p `1 <= E-bound (L~ f) or not S-bound (L~ f) <= p `2 or not p `2 <= N-bound (L~ f) ) } by Th37; then A15: (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) /. n in LeftComp f by A12; A16: 1 <= (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 by NAT_1:11; then A17: (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 in dom g by A10, FINSEQ_3:25; A18: LeftComp f misses RightComp f by SPRECT_1:88; A19: L~ f misses LeftComp f by Th26; A20: len g in dom g by FINSEQ_5:6; A21: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) in L~ f by A5, XBOOLE_0:def_4; now__::_thesis:_not_n_=_1 assume A22: n = 1 ; ::_thesis: contradiction percases ( Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) <> g . ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1) or Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) = g . ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1) ) ; suppose Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) <> g . ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1) ; ::_thesis: contradiction then L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))) = <*(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))*> ^ (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g))) by JORDAN3:def_3; then (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) /. n = Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) by A22, FINSEQ_5:15; hence contradiction by A19, A21, A15, XBOOLE_0:3; ::_thesis: verum end; supposeA23: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) = g . ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1) ; ::_thesis: contradiction then L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))) = mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g)) by JORDAN3:def_3; then (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) /. n = g /. ((1 + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1)) -' 1) by A20, A11, A10, A17, A22, SPRECT_2:3 .= g /. ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1) by NAT_D:34 .= Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) by A17, A23, PARTFUN1:def_6 ; hence contradiction by A19, A21, A15, XBOOLE_0:3; ::_thesis: verum end; end; end; then A24: n > 1 by A13, XXREAL_0:1; then A25: 1 + 1 < (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n by A7, XREAL_1:8; then A26: 1 <= ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 by NAT_D:49; set m = mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n),(len g)); A27: len <*(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))*> = 1 by FINSEQ_1:39; A28: n <= len (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) by A11, FINSEQ_3:25; then A29: n + (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) <= (len (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))))) + (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) by XREAL_1:6; A30: n = (n -' 1) + 1 by A13, XREAL_1:235; then A31: 1 <= n -' 1 by A24, NAT_1:13; A32: len (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g))) = ((len g) -' ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1)) + 1 by A10, A16, JORDAN4:8 .= (len g) -' (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) by A6, JORDAN3:8, NAT_2:7 ; then A33: ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + (len (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g))))) + 1 = (len g) + 1 by A9, XREAL_1:235; now__::_thesis:_not_Last_Point_((L~_g),(g_/._1),(g_/._(len_g)),(L~_f))_<>_g_._((Index_((Last_Point_((L~_g),(g_/._1),(g_/._(len_g)),(L~_f))),g))_+_1) A34: (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 <= ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 by A14, A31, XREAL_1:6; assume A35: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) <> g . ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1) ; ::_thesis: contradiction then A36: L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))) = <*(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))*> ^ (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g))) by JORDAN3:def_3; then A37: len (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) = 1 + (len (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g)))) by A27, FINSEQ_1:22; then A38: ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 <= len g by A33, A29, NAT_D:53; A39: (len (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))))) -' 1 = len (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g))) by A37, NAT_D:34; then n -' 1 <= len (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g))) by A28, NAT_D:42; then A40: n -' 1 in dom (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g))) by A31, FINSEQ_3:25; (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) /. n = (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g))) /. (n -' 1) by A28, A30, A27, A31, A36, A39, NAT_D:42, SEQ_4:136; then A41: (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) /. n = g /. (((n -' 1) + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1)) -' 1) by A20, A10, A17, A40, SPRECT_2:3 .= g /. ((n + (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g))) -' 1) by A30 ; then A42: ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 <> len g by A2, A15, A18, XBOOLE_0:3; then A43: ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 < len g by A38, XXREAL_0:1; reconsider m = mid (g,(((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1),(len g)) as S-Sequence_in_R2 by A4, A26, A38, A42, JORDAN3:6; A44: ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 in dom g by A26, A38, FINSEQ_3:25; then A45: m /. (len m) in RightComp f by A2, A20, SPRECT_2:9; m /. 1 in LeftComp f by A20, A15, A41, A44, SPRECT_2:8; then L~ f meets L~ m by A45, Th33; then consider q being set such that A46: q in L~ f and A47: q in L~ m by XBOOLE_0:3; reconsider q = q as Point of (TOP-REAL 2) by A47; consider i being Element of NAT such that A48: 1 <= i and A49: i + 1 <= len m and A50: q in LSeg (m,i) by A47, SPPOL_2:13; A51: len m = ((len g) -' (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) + 1 by A26, A38, JORDAN4:8; then i <= (len g) -' (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1) by A49, XREAL_1:6; then A52: i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1) <= len g by A38, NAT_D:54; i < len m by A49, NAT_1:13; then A53: LSeg (m,i) = LSeg (g,((i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1)) by A26, A48, A51, A43, JORDAN4:19; set j = (i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1; i <= i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1) by NAT_1:11; then A54: ((i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1) + 1 <= len g by A48, A52, XREAL_1:235, XXREAL_0:2; (i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1 = (i -' 1) + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1) by A48, NAT_D:38; then (i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1 >= ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 by NAT_1:11; then A55: (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 <= (i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1 by A34, XXREAL_0:2; A56: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) <> g /. ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1) by A17, A35, PARTFUN1:def_6; A57: now__::_thesis:_not_Last_Point_((L~_g),(g_/._1),(g_/._(len_g)),(L~_f))_=_q assume Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) = q ; ::_thesis: contradiction then A58: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) in (LSeg (g,(Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)))) /\ (LSeg (g,((i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1))) by A8, A50, A53, XBOOLE_0:def_4; then A59: LSeg (g,(Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g))) meets LSeg (g,((i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1)) by XBOOLE_0:4; percases ( (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 = (i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1 or (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 < (i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1 ) by A55, XXREAL_0:1; supposeA60: (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 = (i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1 ; ::_thesis: contradiction then (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + (1 + 1) <= len g by A54; then (LSeg (g,(Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)))) /\ (LSeg (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1))) = {(g /. ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1))} by A7, TOPREAL1:def_6; hence contradiction by A56, A58, A60, TARSKI:def_1; ::_thesis: verum end; suppose (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 < (i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1 ; ::_thesis: contradiction hence contradiction by A59, TOPREAL1:def_7; ::_thesis: verum end; end; end; 1 <= (i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1 by A16, A55, XXREAL_0:2; then Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g) >= (i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1 by A3, A8, A10, A7, A46, A50, A53, A54, A57, JORDAN5C:28; then Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g) >= (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 by A55, XXREAL_0:2; hence contradiction by XREAL_1:29; ::_thesis: verum end; then A61: L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))) = mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g)) by JORDAN3:def_3; then A62: (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + (len (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))))) = len g by A9, A32, XREAL_1:235; then A63: mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n),(len g)) = g /^ (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1) by A29, FINSEQ_6:117; A64: 1 <= (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n by A25, XXREAL_0:2; (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1) + 1 = (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n by A25, XREAL_1:235, XXREAL_0:2; then ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 < len g by A29, A62, NAT_1:13; then A65: (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n),(len g))) /. (len (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n),(len g)))) in RightComp f by A2, A63, JORDAN4:6; A66: (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) /. n = g /. ((n + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1)) -' 1) by A20, A11, A10, A17, A61, SPRECT_2:3 .= g /. (((n + (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g))) + 1) -' 1) .= g /. ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) by NAT_D:34 ; then A67: (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n <> len g by A2, A15, A18, XBOOLE_0:3; then reconsider m = mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n),(len g)) as S-Sequence_in_R2 by A4, A29, A62, A64, JORDAN3:6; (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n in dom g by A29, A62, A64, FINSEQ_3:25; then m /. 1 in LeftComp f by A20, A15, A66, SPRECT_2:8; then L~ f meets L~ m by A65, Th33; then consider q being set such that A68: q in L~ f and A69: q in L~ m by XBOOLE_0:3; reconsider q = q as Point of (TOP-REAL 2) by A69; consider i being Element of NAT such that A70: 1 <= i and A71: i + 1 <= len m and A72: q in LSeg (m,i) by A69, SPPOL_2:13; set j = (i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1; A73: (i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1 = (i -' 1) + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) by A70, NAT_D:38; then A74: (i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1 >= (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n by NAT_1:11; len m = ((len g) -' ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) + 1 by A4, A29, A62, A64, FINSEQ_6:118; then A75: i < ((len g) -' ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) + 1 by A71, NAT_1:13; then i -' 1 < (len g) -' ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) by A70, NAT_D:54; then (i -' 1) + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) < len g by NAT_D:53; then A76: ((i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1) + 1 <= len g by A73, NAT_1:13; (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n < len g by A29, A62, A67, XXREAL_0:1; then A77: LSeg (m,i) = LSeg (g,((i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1)) by A64, A70, A75, JORDAN4:19; (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 < (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n by A24, XREAL_1:6; then A78: (i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1 > (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 by A74, XXREAL_0:2; A79: now__::_thesis:_not_Last_Point_((L~_g),(g_/._1),(g_/._(len_g)),(L~_f))_=_q assume Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) = q ; ::_thesis: contradiction then Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) in (LSeg (g,(Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)))) /\ (LSeg (g,((i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1))) by A8, A72, A77, XBOOLE_0:def_4; then LSeg (g,(Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g))) meets LSeg (g,((i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1)) by XBOOLE_0:4; hence contradiction by A78, TOPREAL1:def_7; ::_thesis: verum end; 1 <= (i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1 by A64, A74, XXREAL_0:2; then Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g) >= (i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1 by A3, A8, A10, A7, A68, A72, A77, A79, A76, JORDAN5C:28; then Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g) >= (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 by A78, XXREAL_0:2; hence contradiction by XREAL_1:29; ::_thesis: verum end; theorem :: SPRECT_3:55 for i, j being Element of NAT for f being non constant standard special_circular_sequence st 1 <= i & i < len (GoB f) & 1 <= j & j < width (GoB f) holds Int (cell ((GoB f),i,j)) misses L~ (SpStSeq (L~ f)) proof let i, j be Element of NAT ; ::_thesis: for f being non constant standard special_circular_sequence st 1 <= i & i < len (GoB f) & 1 <= j & j < width (GoB f) holds Int (cell ((GoB f),i,j)) misses L~ (SpStSeq (L~ f)) let f be non constant standard special_circular_sequence; ::_thesis: ( 1 <= i & i < len (GoB f) & 1 <= j & j < width (GoB f) implies Int (cell ((GoB f),i,j)) misses L~ (SpStSeq (L~ f)) ) assume that A1: 1 <= i and A2: i < len (GoB f) and A3: 1 <= j and A4: j < width (GoB f) ; ::_thesis: Int (cell ((GoB f),i,j)) misses L~ (SpStSeq (L~ f)) A5: i + 1 <= len (GoB f) by A2, NAT_1:13; set G = GoB f; A6: Int (cell ((GoB f),i,j)) = { |[r,s]| where r, s is Real : ( ((GoB f) * (i,1)) `1 < r & r < ((GoB f) * ((i + 1),1)) `1 & ((GoB f) * (1,j)) `2 < s & s < ((GoB f) * (1,(j + 1))) `2 ) } by A1, A2, A3, A4, GOBOARD6:26; A7: N-bound (L~ (SpStSeq (L~ f))) = N-bound (L~ f) by SPRECT_1:60; A8: 1 <= width (GoB f) by GOBRD11:34; then A9: <*((GoB f) * (i,1))*> is_in_the_area_of f by A1, A2, Th49; 1 <= i + 1 by A1, NAT_1:13; then A10: <*((GoB f) * ((i + 1),1))*> is_in_the_area_of f by A8, A5, Th49; assume Int (cell ((GoB f),i,j)) meets L~ (SpStSeq (L~ f)) ; ::_thesis: contradiction then consider x being set such that A11: x in Int (cell ((GoB f),i,j)) and A12: x in L~ (SpStSeq (L~ f)) by XBOOLE_0:3; A13: W-bound (L~ (SpStSeq (L~ f))) = W-bound (L~ f) by SPRECT_1:58; A14: 1 <= len (GoB f) by GOBRD11:34; then A15: <*((GoB f) * (1,j))*> is_in_the_area_of f by A3, A4, Th49; A16: j + 1 <= width (GoB f) by A4, NAT_1:13; 1 <= j + 1 by A3, NAT_1:13; then A17: <*((GoB f) * (1,(j + 1)))*> is_in_the_area_of f by A14, A16, Th49; A18: L~ (SpStSeq (L~ f)) = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = W-bound (L~ (SpStSeq (L~ f))) & p `2 <= N-bound (L~ (SpStSeq (L~ f))) & p `2 >= S-bound (L~ (SpStSeq (L~ f))) ) or ( p `1 <= E-bound (L~ (SpStSeq (L~ f))) & p `1 >= W-bound (L~ (SpStSeq (L~ f))) & p `2 = N-bound (L~ (SpStSeq (L~ f))) ) or ( p `1 <= E-bound (L~ (SpStSeq (L~ f))) & p `1 >= W-bound (L~ (SpStSeq (L~ f))) & p `2 = S-bound (L~ (SpStSeq (L~ f))) ) or ( p `1 = E-bound (L~ (SpStSeq (L~ f))) & p `2 <= N-bound (L~ (SpStSeq (L~ f))) & p `2 >= S-bound (L~ (SpStSeq (L~ f))) ) ) } by Th35; A19: E-bound (L~ (SpStSeq (L~ f))) = E-bound (L~ f) by SPRECT_1:61; consider p being Point of (TOP-REAL 2) such that A20: p = x and A21: ( ( p `1 = W-bound (L~ (SpStSeq (L~ f))) & p `2 <= N-bound (L~ (SpStSeq (L~ f))) & p `2 >= S-bound (L~ (SpStSeq (L~ f))) ) or ( p `1 <= E-bound (L~ (SpStSeq (L~ f))) & p `1 >= W-bound (L~ (SpStSeq (L~ f))) & p `2 = N-bound (L~ (SpStSeq (L~ f))) ) or ( p `1 <= E-bound (L~ (SpStSeq (L~ f))) & p `1 >= W-bound (L~ (SpStSeq (L~ f))) & p `2 = S-bound (L~ (SpStSeq (L~ f))) ) or ( p `1 = E-bound (L~ (SpStSeq (L~ f))) & p `2 <= N-bound (L~ (SpStSeq (L~ f))) & p `2 >= S-bound (L~ (SpStSeq (L~ f))) ) ) by A12, A18; A22: S-bound (L~ (SpStSeq (L~ f))) = S-bound (L~ f) by SPRECT_1:59; consider r, s being Real such that A23: x = |[r,s]| and A24: ((GoB f) * (i,1)) `1 < r and A25: r < ((GoB f) * ((i + 1),1)) `1 and A26: ((GoB f) * (1,j)) `2 < s and A27: s < ((GoB f) * (1,(j + 1))) `2 by A6, A11; A28: p `1 = r by A23, A20, EUCLID:52; A29: p `2 = s by A23, A20, EUCLID:52; percases ( p `1 = W-bound (L~ (SpStSeq (L~ f))) or p `2 = N-bound (L~ (SpStSeq (L~ f))) or p `2 = S-bound (L~ (SpStSeq (L~ f))) or p `1 = E-bound (L~ (SpStSeq (L~ f))) ) by A21; supposeA30: p `1 = W-bound (L~ (SpStSeq (L~ f))) ; ::_thesis: contradiction A31: 1 in dom <*((GoB f) * (i,1))*> by FINSEQ_5:6; <*((GoB f) * (i,1))*> /. 1 = (GoB f) * (i,1) by FINSEQ_4:16; hence contradiction by A24, A9, A28, A13, A30, A31, SPRECT_2:def_1; ::_thesis: verum end; supposeA32: p `2 = N-bound (L~ (SpStSeq (L~ f))) ; ::_thesis: contradiction A33: 1 in dom <*((GoB f) * (1,(j + 1)))*> by FINSEQ_5:6; <*((GoB f) * (1,(j + 1)))*> /. 1 = (GoB f) * (1,(j + 1)) by FINSEQ_4:16; hence contradiction by A27, A17, A29, A7, A32, A33, SPRECT_2:def_1; ::_thesis: verum end; supposeA34: p `2 = S-bound (L~ (SpStSeq (L~ f))) ; ::_thesis: contradiction A35: 1 in dom <*((GoB f) * (1,j))*> by FINSEQ_5:6; <*((GoB f) * (1,j))*> /. 1 = (GoB f) * (1,j) by FINSEQ_4:16; hence contradiction by A26, A15, A29, A22, A34, A35, SPRECT_2:def_1; ::_thesis: verum end; supposeA36: p `1 = E-bound (L~ (SpStSeq (L~ f))) ; ::_thesis: contradiction A37: 1 in dom <*((GoB f) * ((i + 1),1))*> by FINSEQ_5:6; <*((GoB f) * ((i + 1),1))*> /. 1 = (GoB f) * ((i + 1),1) by FINSEQ_4:16; hence contradiction by A25, A10, A28, A19, A36, A37, SPRECT_2:def_1; ::_thesis: verum end; end; end; theorem :: SPRECT_3:56 for f, g being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st g is_in_the_area_of f & <*p*> is_in_the_area_of f & g is being_S-Seq & p in L~ g holds L_Cut (g,p) is_in_the_area_of f proof let f, g be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st g is_in_the_area_of f & <*p*> is_in_the_area_of f & g is being_S-Seq & p in L~ g holds L_Cut (g,p) is_in_the_area_of f let p be Point of (TOP-REAL 2); ::_thesis: ( g is_in_the_area_of f & <*p*> is_in_the_area_of f & g is being_S-Seq & p in L~ g implies L_Cut (g,p) is_in_the_area_of f ) assume that A1: g is_in_the_area_of f and A2: <*p*> is_in_the_area_of f and A3: g is being_S-Seq ; ::_thesis: ( not p in L~ g or L_Cut (g,p) is_in_the_area_of f ) 2 <= len g by A3, TOPREAL1:def_8; then 1 <= len g by XXREAL_0:2; then A4: len g in dom g by FINSEQ_3:25; assume p in L~ g ; ::_thesis: L_Cut (g,p) is_in_the_area_of f then Index (p,g) < len g by JORDAN3:8; then A5: (Index (p,g)) + 1 <= len g by NAT_1:13; 1 <= (Index (p,g)) + 1 by NAT_1:11; then A6: (Index (p,g)) + 1 in dom g by A5, FINSEQ_3:25; percases ( p <> g . ((Index (p,g)) + 1) or p = g . ((Index (p,g)) + 1) ) ; suppose p <> g . ((Index (p,g)) + 1) ; ::_thesis: L_Cut (g,p) is_in_the_area_of f then A7: L_Cut (g,p) = <*p*> ^ (mid (g,((Index (p,g)) + 1),(len g))) by JORDAN3:def_3; mid (g,((Index (p,g)) + 1),(len g)) is_in_the_area_of f by A1, A4, A6, SPRECT_2:22; hence L_Cut (g,p) is_in_the_area_of f by A2, A7, SPRECT_2:24; ::_thesis: verum end; suppose p = g . ((Index (p,g)) + 1) ; ::_thesis: L_Cut (g,p) is_in_the_area_of f then L_Cut (g,p) = mid (g,((Index (p,g)) + 1),(len g)) by JORDAN3:def_3; hence L_Cut (g,p) is_in_the_area_of f by A1, A4, A6, SPRECT_2:22; ::_thesis: verum end; end; end;