:: GOBOARD9 semantic presentation begin theorem Th1: :: GOBOARD9:1 for GX being TopSpace for A1, A2, B being Subset of GX st A1 is_a_component_of B & A2 is_a_component_of B & not A1 = A2 holds A1 misses A2 proof let GX be TopSpace; ::_thesis: for A1, A2, B being Subset of GX st A1 is_a_component_of B & A2 is_a_component_of B & not A1 = A2 holds A1 misses A2 let A1, A2, B be Subset of GX; ::_thesis: ( A1 is_a_component_of B & A2 is_a_component_of B & not A1 = A2 implies A1 misses A2 ) assume A1 is_a_component_of B ; ::_thesis: ( not A2 is_a_component_of B or A1 = A2 or A1 misses A2 ) then A1: ex B1 being Subset of (GX | B) st ( B1 = A1 & B1 is a_component ) by CONNSP_1:def_6; assume A2 is_a_component_of B ; ::_thesis: ( A1 = A2 or A1 misses A2 ) then ex B2 being Subset of (GX | B) st ( B2 = A2 & B2 is a_component ) by CONNSP_1:def_6; hence ( A1 = A2 or A1 misses A2 ) by A1, CONNSP_1:35; ::_thesis: verum end; theorem Th2: :: GOBOARD9:2 for GX being TopSpace for A, B being Subset of GX for AA being Subset of (GX | B) st A = AA holds GX | A = (GX | B) | AA proof let GX be TopSpace; ::_thesis: for A, B being Subset of GX for AA being Subset of (GX | B) st A = AA holds GX | A = (GX | B) | AA let A, B be Subset of GX; ::_thesis: for AA being Subset of (GX | B) st A = AA holds GX | A = (GX | B) | AA let AA be Subset of (GX | B); ::_thesis: ( A = AA implies GX | A = (GX | B) | AA ) assume A1: A = AA ; ::_thesis: GX | A = (GX | B) | AA the carrier of (GX | A) = [#] (GX | A) .= A by PRE_TOPC:def_5 ; then reconsider GY = GX | A as strict SubSpace of GX | B by A1, TSEP_1:4; [#] GY = AA by A1, PRE_TOPC:def_5; hence GX | A = (GX | B) | AA by PRE_TOPC:def_5; ::_thesis: verum end; theorem Th3: :: GOBOARD9:3 for GX being non empty TopSpace for A, B being non empty Subset of GX st A c= B & A is connected holds ex C being Subset of GX st ( C is_a_component_of B & A c= C ) proof let GX be non empty TopSpace; ::_thesis: for A, B being non empty Subset of GX st A c= B & A is connected holds ex C being Subset of GX st ( C is_a_component_of B & A c= C ) let A, B be non empty Subset of GX; ::_thesis: ( A c= B & A is connected implies ex C being Subset of GX st ( C is_a_component_of B & A c= C ) ) assume that A1: A c= B and A2: A is connected ; ::_thesis: ex C being Subset of GX st ( C is_a_component_of B & A c= C ) consider p being set such that A3: p in A by XBOOLE_0:def_1; A4: B = [#] (GX | B) by PRE_TOPC:def_5 .= the carrier of (GX | B) ; then reconsider p = p as Point of (GX | B) by A1, A3; reconsider C = Component_of p as Subset of GX by PRE_TOPC:11; take C ; ::_thesis: ( C is_a_component_of B & A c= C ) A5: Component_of p is a_component by CONNSP_1:40; hence C is_a_component_of B by CONNSP_1:def_6; ::_thesis: A c= C reconsider AA = A as Subset of (GX | B) by A1, A4; GX | A is connected by A2, CONNSP_1:def_3; then (GX | B) | AA is connected by Th2; then A6: AA is connected by CONNSP_1:def_3; p in Component_of p by CONNSP_1:38; then AA /\ (Component_of p) <> {} (GX | B) by A3, XBOOLE_0:def_4; then AA meets Component_of p by XBOOLE_0:def_7; hence A c= C by A5, A6, CONNSP_1:36; ::_thesis: verum end; theorem Th4: :: GOBOARD9:4 for GX being non empty TopSpace for A, B, C, D being Subset of GX st B is connected & C is_a_component_of D & A c= C & A meets B & B c= D holds B c= C proof let GX be non empty TopSpace; ::_thesis: for A, B, C, D being Subset of GX st B is connected & C is_a_component_of D & A c= C & A meets B & B c= D holds B c= C let A, B, C, D be Subset of GX; ::_thesis: ( B is connected & C is_a_component_of D & A c= C & A meets B & B c= D implies B c= C ) assume that A1: B is connected and A2: C is_a_component_of D and A3: A c= C and A4: A meets B and A5: B c= D ; ::_thesis: B c= C A6: A <> {} by A4, XBOOLE_1:65; A7: B <> {} by A4, XBOOLE_1:65; reconsider A = A, B = B as non empty Subset of GX by A4, XBOOLE_1:65; reconsider C = C, D = D as non empty Subset of GX by A3, A5, A6, A7, XBOOLE_1:3; consider CC being Subset of GX such that A8: CC is_a_component_of D and A9: B c= CC by A1, A5, Th3; A10: A meets CC by A4, A9, XBOOLE_1:63; A11: ex C1 being Subset of (GX | D) st ( C1 = C & C1 is a_component ) by A2, CONNSP_1:def_6; ex CC1 being Subset of (GX | D) st ( CC1 = CC & CC1 is a_component ) by A8, CONNSP_1:def_6; hence B c= C by A3, A9, A10, A11, CONNSP_1:35, XBOOLE_1:63; ::_thesis: verum end; registration cluster non empty convex for Element of K6( the carrier of (TOP-REAL 2)); existence ex b1 being Subset of (TOP-REAL 2) st ( b1 is convex & not b1 is empty ) proof set p = the Point of (TOP-REAL 2); take LSeg ( the Point of (TOP-REAL 2), the Point of (TOP-REAL 2)) ; ::_thesis: ( LSeg ( the Point of (TOP-REAL 2), the Point of (TOP-REAL 2)) is convex & not LSeg ( the Point of (TOP-REAL 2), the Point of (TOP-REAL 2)) is empty ) thus ( LSeg ( the Point of (TOP-REAL 2), the Point of (TOP-REAL 2)) is convex & not LSeg ( the Point of (TOP-REAL 2), the Point of (TOP-REAL 2)) is empty ) ; ::_thesis: verum end; end; theorem :: GOBOARD9:5 canceled; theorem Th6: :: GOBOARD9:6 for P, Q being convex Subset of (TOP-REAL 2) holds P /\ Q is convex proof let P, Q be convex Subset of (TOP-REAL 2); ::_thesis: P /\ Q is convex let p be Point of (TOP-REAL 2); :: according to JORDAN1:def_1 ::_thesis: for b1 being Element of the carrier of (TOP-REAL 2) holds ( not p in P /\ Q or not b1 in P /\ Q or LSeg (p,b1) c= P /\ Q ) let q be Point of (TOP-REAL 2); ::_thesis: ( not p in P /\ Q or not q in P /\ Q or LSeg (p,q) c= P /\ Q ) assume that A1: p in P /\ Q and A2: q in P /\ Q ; ::_thesis: LSeg (p,q) c= P /\ Q A3: p in P by A1, XBOOLE_0:def_4; q in P by A2, XBOOLE_0:def_4; then A4: LSeg (p,q) c= P by A3, JORDAN1:def_1; A5: p in Q by A1, XBOOLE_0:def_4; q in Q by A2, XBOOLE_0:def_4; then LSeg (p,q) c= Q by A5, JORDAN1:def_1; hence LSeg (p,q) c= P /\ Q by A4, XBOOLE_1:19; ::_thesis: verum end; theorem Th7: :: GOBOARD9:7 for f being FinSequence of (TOP-REAL 2) holds Rev (X_axis f) = X_axis (Rev f) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: Rev (X_axis f) = X_axis (Rev f) A1: len (Rev (X_axis f)) = len (X_axis f) by FINSEQ_5:def_3 .= len f by GOBOARD1:def_1 .= len (Rev f) by FINSEQ_5:def_3 ; len (X_axis f) = len f by GOBOARD1:def_1; then A2: dom (X_axis f) = dom f by FINSEQ_3:29; A3: len f = len (Rev f) by FINSEQ_5:def_3; now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_(Rev_(X_axis_f))_holds_ (Rev_(X_axis_f))_._k_=_((Rev_f)_/._k)_`1 let k be Element of NAT ; ::_thesis: ( k in dom (Rev (X_axis f)) implies (Rev (X_axis f)) . k = ((Rev f) /. k) `1 ) assume A4: k in dom (Rev (X_axis f)) ; ::_thesis: (Rev (X_axis f)) . k = ((Rev f) /. k) `1 set l = ((len f) + 1) -' k; A5: k <= len f by A1, A3, A4, FINSEQ_3:25; len f < (len f) + 1 by NAT_1:13; then A6: (((len f) + 1) -' k) + k = (len f) + 1 by A5, XREAL_1:235, XXREAL_0:2; A7: Rev (Rev (X_axis f)) = X_axis f ; then A8: ((len f) + 1) -' k in dom (X_axis f) by A1, A3, A4, A6, FINSEQ_5:59; thus (Rev (X_axis f)) . k = (Rev (X_axis f)) /. k by A4, PARTFUN1:def_6 .= (X_axis f) /. (((len f) + 1) -' k) by A1, A3, A4, A6, A7, FINSEQ_5:66 .= (X_axis f) . (((len f) + 1) -' k) by A8, PARTFUN1:def_6 .= (f /. (((len f) + 1) -' k)) `1 by A8, GOBOARD1:def_1 .= ((Rev f) /. k) `1 by A1, A2, A3, A4, A6, A7, FINSEQ_5:59, FINSEQ_5:66 ; ::_thesis: verum end; hence Rev (X_axis f) = X_axis (Rev f) by A1, GOBOARD1:def_1; ::_thesis: verum end; theorem Th8: :: GOBOARD9:8 for f being FinSequence of (TOP-REAL 2) holds Rev (Y_axis f) = Y_axis (Rev f) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: Rev (Y_axis f) = Y_axis (Rev f) A1: len (Rev (Y_axis f)) = len (Y_axis f) by FINSEQ_5:def_3 .= len f by GOBOARD1:def_2 .= len (Rev f) by FINSEQ_5:def_3 ; len (Y_axis f) = len f by GOBOARD1:def_2; then A2: dom (Y_axis f) = dom f by FINSEQ_3:29; A3: len f = len (Rev f) by FINSEQ_5:def_3; now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_(Rev_(Y_axis_f))_holds_ (Rev_(Y_axis_f))_._k_=_((Rev_f)_/._k)_`2 let k be Element of NAT ; ::_thesis: ( k in dom (Rev (Y_axis f)) implies (Rev (Y_axis f)) . k = ((Rev f) /. k) `2 ) assume A4: k in dom (Rev (Y_axis f)) ; ::_thesis: (Rev (Y_axis f)) . k = ((Rev f) /. k) `2 set l = ((len f) + 1) -' k; A5: k <= len f by A1, A3, A4, FINSEQ_3:25; len f < (len f) + 1 by NAT_1:13; then A6: (((len f) + 1) -' k) + k = (len f) + 1 by A5, XREAL_1:235, XXREAL_0:2; A7: Rev (Rev (Y_axis f)) = Y_axis f ; then A8: ((len f) + 1) -' k in dom (Y_axis f) by A1, A3, A4, A6, FINSEQ_5:59; thus (Rev (Y_axis f)) . k = (Rev (Y_axis f)) /. k by A4, PARTFUN1:def_6 .= (Y_axis f) /. (((len f) + 1) -' k) by A1, A3, A4, A6, A7, FINSEQ_5:66 .= (Y_axis f) . (((len f) + 1) -' k) by A8, PARTFUN1:def_6 .= (f /. (((len f) + 1) -' k)) `2 by A8, GOBOARD1:def_2 .= ((Rev f) /. k) `2 by A1, A2, A3, A4, A6, A7, FINSEQ_5:59, FINSEQ_5:66 ; ::_thesis: verum end; hence Rev (Y_axis f) = Y_axis (Rev f) by A1, GOBOARD1:def_2; ::_thesis: verum end; Lm1: for f, ff being non empty FinSequence of (TOP-REAL 2) st ff = Rev f holds GoB ff = GoB f proof let f, ff be non empty FinSequence of (TOP-REAL 2); ::_thesis: ( ff = Rev f implies GoB ff = GoB f ) assume A1: ff = Rev f ; ::_thesis: GoB ff = GoB f then A2: Rev (X_axis f) = X_axis ff by Th7; A3: rng (Incr (X_axis ff)) = rng (X_axis ff) by SEQ_4:def_21 .= rng (X_axis f) by A2, FINSEQ_5:57 ; len (Incr (X_axis ff)) = card (rng (X_axis ff)) by SEQ_4:def_21 .= card (rng (X_axis f)) by A2, FINSEQ_5:57 ; then A4: Incr (X_axis f) = Incr (X_axis ff) by A3, SEQ_4:def_21; A5: Rev (Y_axis f) = Y_axis ff by A1, Th8; A6: rng (Incr (Y_axis ff)) = rng (Y_axis ff) by SEQ_4:def_21 .= rng (Y_axis f) by A5, FINSEQ_5:57 ; len (Incr (Y_axis ff)) = card (rng (Y_axis ff)) by SEQ_4:def_21 .= card (rng (Y_axis f)) by A5, FINSEQ_5:57 ; then Incr (Y_axis f) = Incr (Y_axis ff) by A6, SEQ_4:def_21; hence GoB ff = GoB ((Incr (X_axis f)),(Incr (Y_axis f))) by A4, GOBOARD2:def_2 .= GoB f by GOBOARD2:def_2 ; ::_thesis: verum end; registration clusterV13() V16( NAT ) Function-like non constant V26() FinSequence-like FinSubsequence-like for set ; existence not for b1 being FinSequence holds b1 is constant proof take <*1,2*> ; ::_thesis: not <*1,2*> is constant take 1 ; :: according to SEQM_3:def_10 ::_thesis: ex b1 being Element of NAT st ( 1 in dom <*1,2*> & b1 in dom <*1,2*> & not <*1,2*> . 1 = <*1,2*> . b1 ) take 2 ; ::_thesis: ( 1 in dom <*1,2*> & 2 in dom <*1,2*> & not <*1,2*> . 1 = <*1,2*> . 2 ) A1: 1 in {1,2} by TARSKI:def_2; 2 in {1,2} by TARSKI:def_2; hence ( 1 in dom <*1,2*> & 2 in dom <*1,2*> ) by A1, FINSEQ_1:2, FINSEQ_1:89; ::_thesis: not <*1,2*> . 1 = <*1,2*> . 2 <*1,2*> . 1 = 1 by FINSEQ_1:44; hence not <*1,2*> . 1 = <*1,2*> . 2 by FINSEQ_1:44; ::_thesis: verum end; end; registration let f be non constant FinSequence; cluster Rev f -> non constant ; coherence not Rev f is constant proof consider i, j being Element of NAT such that A1: i in dom f and A2: j in dom f and A3: f . i <> f . j by SEQM_3:def_10; A4: i <= len f by A1, FINSEQ_3:25; j <= len f by A2, FINSEQ_3:25; then reconsider k1 = (len f) - i, l1 = (len f) - j as Element of NAT by A4, INT_1:5; take k = k1 + 1; :: according to SEQM_3:def_10 ::_thesis: ex b1 being Element of NAT st ( k in dom (Rev f) & b1 in dom (Rev f) & not (Rev f) . k = (Rev f) . b1 ) take l = l1 + 1; ::_thesis: ( k in dom (Rev f) & l in dom (Rev f) & not (Rev f) . k = (Rev f) . l ) k + i = (len f) + 1 ; hence k in dom (Rev f) by A1, FINSEQ_5:59; ::_thesis: ( l in dom (Rev f) & not (Rev f) . k = (Rev f) . l ) then A5: (Rev f) . k = f . (((len f) - k) + 1) by FINSEQ_5:def_3 .= f . (0 + i) ; l + j = (len f) + 1 ; hence l in dom (Rev f) by A2, FINSEQ_5:59; ::_thesis: not (Rev f) . k = (Rev f) . l then (Rev f) . l = f . (((len f) - l) + 1) by FINSEQ_5:def_3 .= f . (0 + j) ; hence not (Rev f) . k = (Rev f) . l by A3, A5; ::_thesis: verum end; end; definition let f be standard special_circular_sequence; :: original: Rev redefine func Rev f -> standard special_circular_sequence; coherence Rev f is standard special_circular_sequence proof reconsider ff = Rev f as non empty FinSequence of (TOP-REAL 2) ; A1: Rev ff = f ; A2: GoB ff = GoB f by Lm1; A3: f is_sequence_on GoB f by GOBOARD5:def_5; A4: len f = len ff by FINSEQ_5:def_3; A5: ff is standard proof hereby :: according to GOBOARD5:def_5,GOBOARD1:def_9 ::_thesis: for b1 being Element of NAT holds ( not b1 in dom ff or not b1 + 1 in dom ff or for b2, b3, b4, b5 being Element of NAT holds ( not [b2,b3] in Indices (GoB ff) or not [b4,b5] in Indices (GoB ff) or not ff /. b1 = (GoB ff) * (b2,b3) or not ff /. (b1 + 1) = (GoB ff) * (b4,b5) or K36((abs K40(b2,b4)),(abs K40(b3,b5))) = 1 ) ) let k be Element of NAT ; ::_thesis: ( k in dom ff implies ex i, j being Element of NAT st ( [i,j] in Indices (GoB ff) & ff /. k = (GoB ff) * (i,j) ) ) assume A6: k in dom ff ; ::_thesis: ex i, j being Element of NAT st ( [i,j] in Indices (GoB ff) & ff /. k = (GoB ff) * (i,j) ) set l = ((len f) + 1) -' k; A7: k <= len f by A4, A6, FINSEQ_3:25; len f < (len f) + 1 by NAT_1:13; then A8: (((len f) + 1) -' k) + k = (len f) + 1 by A7, XREAL_1:235, XXREAL_0:2; then ((len f) + 1) -' k in dom f by A1, A4, A6, FINSEQ_5:59; then consider i, j being Element of NAT such that A9: [i,j] in Indices (GoB f) and A10: f /. (((len f) + 1) -' k) = (GoB f) * (i,j) by A3, GOBOARD1:def_9; take i = i; ::_thesis: ex j being Element of NAT st ( [i,j] in Indices (GoB ff) & ff /. k = (GoB ff) * (i,j) ) take j = j; ::_thesis: ( [i,j] in Indices (GoB ff) & ff /. k = (GoB ff) * (i,j) ) thus [i,j] in Indices (GoB ff) by A9, Lm1; ::_thesis: ff /. k = (GoB ff) * (i,j) thus ff /. k = (GoB ff) * (i,j) by A1, A2, A4, A6, A8, A10, FINSEQ_5:66; ::_thesis: verum end; let k be Element of NAT ; ::_thesis: ( not k in dom ff or not k + 1 in dom ff or for b1, b2, b3, b4 being Element of NAT holds ( not [b1,b2] in Indices (GoB ff) or not [b3,b4] in Indices (GoB ff) or not ff /. k = (GoB ff) * (b1,b2) or not ff /. (k + 1) = (GoB ff) * (b3,b4) or K36((abs K40(b1,b3)),(abs K40(b2,b4))) = 1 ) ) assume that A11: k in dom ff and A12: k + 1 in dom ff ; ::_thesis: for b1, b2, b3, b4 being Element of NAT holds ( not [b1,b2] in Indices (GoB ff) or not [b3,b4] in Indices (GoB ff) or not ff /. k = (GoB ff) * (b1,b2) or not ff /. (k + 1) = (GoB ff) * (b3,b4) or K36((abs K40(b1,b3)),(abs K40(b2,b4))) = 1 ) set l = ((len f) + 1) -' (k + 1); k <= len f by A4, A11, FINSEQ_3:25; then k + 1 <= (len f) + 1 by XREAL_1:6; then A13: (((len f) + 1) -' (k + 1)) + (k + 1) = (len f) + 1 by XREAL_1:235; then A14: ((len f) + 1) -' (k + 1) in dom f by A1, A4, A12, FINSEQ_5:59; A15: ((((len f) + 1) -' (k + 1)) + 1) + k = (len f) + 1 by A13; then A16: (((len f) + 1) -' (k + 1)) + 1 in dom f by A1, A4, A11, FINSEQ_5:59; let i1, j1, i2, j2 be Element of NAT ; ::_thesis: ( not [i1,j1] in Indices (GoB ff) or not [i2,j2] in Indices (GoB ff) or not ff /. k = (GoB ff) * (i1,j1) or not ff /. (k + 1) = (GoB ff) * (i2,j2) or K36((abs K40(i1,i2)),(abs K40(j1,j2))) = 1 ) assume that A17: [i1,j1] in Indices (GoB ff) and A18: [i2,j2] in Indices (GoB ff) and A19: ff /. k = (GoB ff) * (i1,j1) and A20: ff /. (k + 1) = (GoB ff) * (i2,j2) ; ::_thesis: K36((abs K40(i1,i2)),(abs K40(j1,j2))) = 1 A21: abs (i2 - i1) = abs (- (i1 - i2)) .= abs (i1 - i2) by COMPLEX1:52 ; A22: abs (j2 - j1) = abs (- (j1 - j2)) .= abs (j1 - j2) by COMPLEX1:52 ; A23: f /. (((len f) + 1) -' (k + 1)) = (GoB f) * (i2,j2) by A1, A2, A4, A12, A13, A20, FINSEQ_5:66; f /. ((((len f) + 1) -' (k + 1)) + 1) = (GoB f) * (i1,j1) by A1, A2, A4, A11, A15, A19, FINSEQ_5:66; hence (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A2, A3, A14, A16, A17, A18, A21, A22, A23, GOBOARD1:def_9; ::_thesis: verum end; A24: ff /. 1 = f /. (len f) by FINSEQ_5:65 .= f /. 1 by FINSEQ_6:def_1 .= ff /. (len ff) by A4, FINSEQ_5:65 ; ff is s.c.c. proof let i be Element of NAT ; :: according to GOBOARD5:def_4 ::_thesis: for b1 being Element of NAT holds ( b1 <= i + 1 or ( ( i <= 1 or len ff <= b1 ) & len ff <= b1 + 1 ) or LSeg (ff,i) misses LSeg (ff,b1) ) let j be Element of NAT ; ::_thesis: ( j <= i + 1 or ( ( i <= 1 or len ff <= j ) & len ff <= j + 1 ) or LSeg (ff,i) misses LSeg (ff,j) ) assume that A25: i + 1 < j and A26: ( ( i > 1 & j < len ff ) or j + 1 < len ff ) ; ::_thesis: LSeg (ff,i) misses LSeg (ff,j) set k = (len f) -' i; set l = (len f) -' j; A27: j <= len f by A4, A26, NAT_1:13; then A28: ((len f) -' j) + j = len f by XREAL_1:235; i < j by A25, NAT_1:13; then A29: ((len f) -' i) + i = len f by A27, XREAL_1:235, XXREAL_0:2; then (i + 1) + ((len f) -' i) = (((len f) -' j) + 1) + j by A28; then (((len f) -' j) + 1) + j < j + ((len f) -' i) by A25, XREAL_1:6; then A30: ((len f) -' j) + 1 < (len f) -' i by XREAL_1:6; A31: j + 1 <= len f by A4, A26, NAT_1:13; percases ( j + 1 = len f or ( i >= 1 & j + 1 < len f ) or i = 0 ) by A31, NAT_1:14, XXREAL_0:1; suppose j + 1 = len f ; ::_thesis: LSeg (ff,i) misses LSeg (ff,j) then ((len f) -' i) + 1 < len f by A26, A29, FINSEQ_5:def_3, XREAL_1:6; then LSeg (f,((len f) -' i)) misses LSeg (f,((len f) -' j)) by A30, GOBOARD5:def_4; then A32: (LSeg (f,((len f) -' i))) /\ (LSeg (f,((len f) -' j))) = {} by XBOOLE_0:def_7; LSeg (f,((len f) -' i)) = LSeg (ff,i) by A29, SPPOL_2:2; hence (LSeg (ff,i)) /\ (LSeg (ff,j)) = {} by A28, A32, SPPOL_2:2; :: according to XBOOLE_0:def_7 ::_thesis: verum end; supposethat A33: i >= 1 and A34: j + 1 < len f ; ::_thesis: LSeg (ff,i) misses LSeg (ff,j) A35: (len f) -' j > 1 by A28, A34, XREAL_1:6; ((len f) -' i) + 1 <= len f by A29, A33, XREAL_1:6; then (len f) -' i < len f by NAT_1:13; then LSeg (f,((len f) -' i)) misses LSeg (f,((len f) -' j)) by A30, A35, GOBOARD5:def_4; then A36: (LSeg (f,((len f) -' i))) /\ (LSeg (f,((len f) -' j))) = {} by XBOOLE_0:def_7; LSeg (f,((len f) -' i)) = LSeg (ff,i) by A29, SPPOL_2:2; hence (LSeg (ff,i)) /\ (LSeg (ff,j)) = {} by A28, A36, SPPOL_2:2; :: according to XBOOLE_0:def_7 ::_thesis: verum end; suppose i = 0 ; ::_thesis: LSeg (ff,i) misses LSeg (ff,j) then LSeg (ff,i) = {} by TOPREAL1:def_3; hence (LSeg (ff,i)) /\ (LSeg (ff,j)) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: verum end; end; end; hence Rev f is standard special_circular_sequence by A5, A24, FINSEQ_6:def_1, SPPOL_2:28, SPPOL_2:40; ::_thesis: verum end; end; theorem Th9: :: GOBOARD9:9 for f being non constant standard special_circular_sequence for i, j being Element of NAT st i >= 1 & j >= 1 & i + j = len f holds left_cell (f,i) = right_cell ((Rev f),j) proof let f be non constant standard special_circular_sequence; ::_thesis: for i, j being Element of NAT st i >= 1 & j >= 1 & i + j = len f holds left_cell (f,i) = right_cell ((Rev f),j) let i, j be Element of NAT ; ::_thesis: ( i >= 1 & j >= 1 & i + j = len f implies left_cell (f,i) = right_cell ((Rev f),j) ) assume that A1: i >= 1 and A2: j >= 1 and A3: i + j = len f ; ::_thesis: left_cell (f,i) = right_cell ((Rev f),j) A4: i + 1 <= len f by A2, A3, XREAL_1:6; len f = len (Rev f) by FINSEQ_5:def_3; then A5: j + 1 <= len (Rev f) by A1, A3, XREAL_1:6; A6: GoB (Rev f) = GoB f by Lm1; now__::_thesis:_for_i1,_j1,_i2,_j2_being_Element_of_NAT_st_[i1,j1]_in_Indices_(GoB_f)_&_[i2,j2]_in_Indices_(GoB_f)_&_f_/._i_=_(GoB_f)_*_(i1,j1)_&_f_/._(i_+_1)_=_(GoB_f)_*_(i2,j2)_&_not_(_i1_=_i2_&_j1_+_1_=_j2_&_right_cell_((Rev_f),j)_=_cell_((GoB_f),(i1_-'_1),j1)_)_&_not_(_i1_+_1_=_i2_&_j1_=_j2_&_right_cell_((Rev_f),j)_=_cell_((GoB_f),i1,j1)_)_&_not_(_i1_=_i2_+_1_&_j1_=_j2_&_right_cell_((Rev_f),j)_=_cell_((GoB_f),i2,(j2_-'_1))_)_holds_ (_i1_=_i2_&_j1_=_j2_+_1_&_right_cell_((Rev_f),j)_=_cell_((GoB_f),i1,j2)_) let i1, j1, i2, j2 be Element of NAT ; ::_thesis: ( [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. i = (GoB f) * (i1,j1) & f /. (i + 1) = (GoB f) * (i2,j2) & not ( b1 = b3 & b2 + 1 = b4 & right_cell ((Rev f),j) = cell ((GoB f),(b1 -' 1),b2) ) & not ( b1 + 1 = b3 & b2 = b4 & right_cell ((Rev f),j) = cell ((GoB f),b1,b2) ) & not ( b1 = b3 + 1 & b2 = b4 & right_cell ((Rev f),j) = cell ((GoB f),b3,(b4 -' 1)) ) implies ( b1 = b3 & b2 = b4 + 1 & right_cell ((Rev f),j) = cell ((GoB f),b1,b4) ) ) assume that A7: [i1,j1] in Indices (GoB f) and A8: [i2,j2] in Indices (GoB f) and A9: f /. i = (GoB f) * (i1,j1) and A10: f /. (i + 1) = (GoB f) * (i2,j2) ; ::_thesis: ( ( b1 = b3 & b2 + 1 = b4 & right_cell ((Rev f),j) = cell ((GoB f),(b1 -' 1),b2) ) or ( b1 + 1 = b3 & b2 = b4 & right_cell ((Rev f),j) = cell ((GoB f),b1,b2) ) or ( b1 = b3 + 1 & b2 = b4 & right_cell ((Rev f),j) = cell ((GoB f),b3,(b4 -' 1)) ) or ( b1 = b3 & b2 = b4 + 1 & right_cell ((Rev f),j) = cell ((GoB f),b1,b4) ) ) 1 <= i + 1 by NAT_1:11; then A11: i + 1 in dom f by A4, FINSEQ_3:25; (i + 1) + j = (len f) + 1 by A3; then A12: (Rev f) /. j = (GoB f) * (i2,j2) by A10, A11, FINSEQ_5:66; i <= len f by A4, NAT_1:13; then A13: i in dom f by A1, FINSEQ_3:25; (j + 1) + i = (len f) + 1 by A3; then A14: (Rev f) /. (j + 1) = (GoB f) * (i1,j1) by A9, A13, FINSEQ_5:66; 1 <= i1 by A7, MATRIX_1:38; then A15: (i1 -' 1) + 1 = i1 by XREAL_1:235; 1 <= j1 by A7, MATRIX_1:38; then A16: (j1 -' 1) + 1 = j1 by XREAL_1:235; reconsider i19 = i1, i29 = i2, j19 = j1, j29 = j2 as Element of REAL ; f is_sequence_on GoB f by GOBOARD5:def_5; then (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A7, A8, A9, A10, A11, A13, GOBOARD1:def_9; then A17: ( ( abs (i19 - i29) = 1 & j1 = j2 ) or ( abs (j19 - j29) = 1 & i1 = i2 ) ) by SEQM_3:42; percases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A17, SEQM_3:41; case ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: right_cell ((Rev f),j) = cell ((GoB f),(i1 -' 1),j1) hence right_cell ((Rev f),j) = cell ((GoB f),(i1 -' 1),j1) by A2, A5, A6, A7, A8, A12, A14, A15, GOBOARD5:30; ::_thesis: verum end; case ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: right_cell ((Rev f),j) = cell ((GoB f),i1,j1) hence right_cell ((Rev f),j) = cell ((GoB f),i1,j1) by A2, A5, A6, A7, A8, A12, A14, A16, GOBOARD5:29; ::_thesis: verum end; case ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: right_cell ((Rev f),j) = cell ((GoB f),i2,(j2 -' 1)) hence right_cell ((Rev f),j) = cell ((GoB f),i2,(j2 -' 1)) by A2, A5, A6, A7, A8, A12, A14, A16, GOBOARD5:28; ::_thesis: verum end; case ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: right_cell ((Rev f),j) = cell ((GoB f),i1,j2) hence right_cell ((Rev f),j) = cell ((GoB f),i1,j2) by A2, A5, A6, A7, A8, A12, A14, A15, GOBOARD5:27; ::_thesis: verum end; end; end; hence left_cell (f,i) = right_cell ((Rev f),j) by A1, A4, GOBOARD5:def_7; ::_thesis: verum end; theorem Th10: :: GOBOARD9:10 for f being non constant standard special_circular_sequence for i, j being Element of NAT st i >= 1 & j >= 1 & i + j = len f holds left_cell ((Rev f),i) = right_cell (f,j) proof let f be non constant standard special_circular_sequence; ::_thesis: for i, j being Element of NAT st i >= 1 & j >= 1 & i + j = len f holds left_cell ((Rev f),i) = right_cell (f,j) let i, j be Element of NAT ; ::_thesis: ( i >= 1 & j >= 1 & i + j = len f implies left_cell ((Rev f),i) = right_cell (f,j) ) A1: len (Rev f) = len f by FINSEQ_5:def_3; Rev (Rev f) = f ; hence ( i >= 1 & j >= 1 & i + j = len f implies left_cell ((Rev f),i) = right_cell (f,j) ) by A1, Th9; ::_thesis: verum end; theorem Th11: :: GOBOARD9:11 for f being non constant standard special_circular_sequence for k being Element of NAT st 1 <= k & k + 1 <= len f holds ex i, j being Element of NAT st ( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) ) proof let f be non constant standard special_circular_sequence; ::_thesis: for k being Element of NAT st 1 <= k & k + 1 <= len f holds ex i, j being Element of NAT st ( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) ) let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f implies ex i, j being Element of NAT st ( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) ) ) assume that A1: 1 <= k and A2: k + 1 <= len f ; ::_thesis: ex i, j being Element of NAT st ( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) ) A3: f is_sequence_on GoB f by GOBOARD5:def_5; k <= len f by A2, NAT_1:13; then A4: k in dom f by A1, FINSEQ_3:25; then consider i1, j1 being Element of NAT such that A5: [i1,j1] in Indices (GoB f) and A6: f /. k = (GoB f) * (i1,j1) by A3, GOBOARD1:def_9; 1 <= k + 1 by NAT_1:11; then A7: k + 1 in dom f by A2, FINSEQ_3:25; then consider i2, j2 being Element of NAT such that A8: [i2,j2] in Indices (GoB f) and A9: f /. (k + 1) = (GoB f) * (i2,j2) by A3, GOBOARD1:def_9; 1 <= i1 by A5, MATRIX_1:38; then A10: (i1 -' 1) + 1 = i1 by XREAL_1:235; 1 <= j1 by A5, MATRIX_1:38; then A11: (j1 -' 1) + 1 = j1 by XREAL_1:235; reconsider i19 = i1, i29 = i2, j19 = j1, j29 = j2 as Element of REAL ; (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A3, A4, A5, A6, A7, A8, A9, GOBOARD1:def_9; then A12: ( ( abs (i19 - i29) = 1 & j1 = j2 ) or ( abs (j19 - j29) = 1 & i1 = i2 ) ) by SEQM_3:42; A13: i1 <= len (GoB f) by A5, MATRIX_1:38; A14: j1 <= width (GoB f) by A5, MATRIX_1:38; percases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A12, SEQM_3:41; supposeA15: ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: ex i, j being Element of NAT st ( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) ) take i1 -' 1 ; ::_thesis: ex j being Element of NAT st ( i1 -' 1 <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),(i1 -' 1),j) = left_cell (f,k) ) take j1 ; ::_thesis: ( i1 -' 1 <= len (GoB f) & j1 <= width (GoB f) & cell ((GoB f),(i1 -' 1),j1) = left_cell (f,k) ) i1 -' 1 <= i1 by NAT_D:35; hence i1 -' 1 <= len (GoB f) by A13, XXREAL_0:2; ::_thesis: ( j1 <= width (GoB f) & cell ((GoB f),(i1 -' 1),j1) = left_cell (f,k) ) thus j1 <= width (GoB f) by A5, MATRIX_1:38; ::_thesis: cell ((GoB f),(i1 -' 1),j1) = left_cell (f,k) thus cell ((GoB f),(i1 -' 1),j1) = left_cell (f,k) by A1, A2, A5, A6, A8, A9, A10, A15, GOBOARD5:27; ::_thesis: verum end; supposeA16: ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: ex i, j being Element of NAT st ( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) ) take i1 ; ::_thesis: ex j being Element of NAT st ( i1 <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i1,j) = left_cell (f,k) ) take j1 ; ::_thesis: ( i1 <= len (GoB f) & j1 <= width (GoB f) & cell ((GoB f),i1,j1) = left_cell (f,k) ) thus i1 <= len (GoB f) by A5, MATRIX_1:38; ::_thesis: ( j1 <= width (GoB f) & cell ((GoB f),i1,j1) = left_cell (f,k) ) thus j1 <= width (GoB f) by A5, MATRIX_1:38; ::_thesis: cell ((GoB f),i1,j1) = left_cell (f,k) thus cell ((GoB f),i1,j1) = left_cell (f,k) by A1, A2, A5, A6, A8, A9, A11, A16, GOBOARD5:28; ::_thesis: verum end; supposeA17: ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: ex i, j being Element of NAT st ( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) ) take i2 ; ::_thesis: ex j being Element of NAT st ( i2 <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i2,j) = left_cell (f,k) ) take j1 -' 1 ; ::_thesis: ( i2 <= len (GoB f) & j1 -' 1 <= width (GoB f) & cell ((GoB f),i2,(j1 -' 1)) = left_cell (f,k) ) thus i2 <= len (GoB f) by A8, MATRIX_1:38; ::_thesis: ( j1 -' 1 <= width (GoB f) & cell ((GoB f),i2,(j1 -' 1)) = left_cell (f,k) ) j1 -' 1 <= j1 by NAT_D:35; hence j1 -' 1 <= width (GoB f) by A14, XXREAL_0:2; ::_thesis: cell ((GoB f),i2,(j1 -' 1)) = left_cell (f,k) thus cell ((GoB f),i2,(j1 -' 1)) = left_cell (f,k) by A1, A2, A5, A6, A8, A9, A11, A17, GOBOARD5:29; ::_thesis: verum end; supposeA18: ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: ex i, j being Element of NAT st ( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) ) take i1 ; ::_thesis: ex j being Element of NAT st ( i1 <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i1,j) = left_cell (f,k) ) take j2 ; ::_thesis: ( i1 <= len (GoB f) & j2 <= width (GoB f) & cell ((GoB f),i1,j2) = left_cell (f,k) ) thus i1 <= len (GoB f) by A5, MATRIX_1:38; ::_thesis: ( j2 <= width (GoB f) & cell ((GoB f),i1,j2) = left_cell (f,k) ) thus j2 <= width (GoB f) by A8, MATRIX_1:38; ::_thesis: cell ((GoB f),i1,j2) = left_cell (f,k) thus cell ((GoB f),i1,j2) = left_cell (f,k) by A1, A2, A5, A6, A8, A9, A10, A18, GOBOARD5:30; ::_thesis: verum end; end; end; theorem Th12: :: GOBOARD9:12 for j being Element of NAT for G being Go-board st j <= width G holds Int (h_strip (G,j)) is convex proof let j be Element of NAT ; ::_thesis: for G being Go-board st j <= width G holds Int (h_strip (G,j)) is convex let G be Go-board; ::_thesis: ( j <= width G implies Int (h_strip (G,j)) is convex ) assume A1: j <= width G ; ::_thesis: Int (h_strip (G,j)) is convex percases ( j = 0 or j = width G or ( 1 <= j & j < width G ) ) by A1, NAT_1:14, XXREAL_0:1; suppose j = 0 ; ::_thesis: Int (h_strip (G,j)) is convex then Int (h_strip (G,j)) = { |[r,s]| where r, s is Real : s < (G * (1,1)) `2 } by GOBOARD6:15; hence Int (h_strip (G,j)) is convex by JORDAN1:17; ::_thesis: verum end; suppose j = width G ; ::_thesis: Int (h_strip (G,j)) is convex then Int (h_strip (G,j)) = { |[r,s]| where r, s is Real : (G * (1,(width G))) `2 < s } by GOBOARD6:16; hence Int (h_strip (G,j)) is convex by JORDAN1:15; ::_thesis: verum end; suppose ( 1 <= j & j < width G ) ; ::_thesis: Int (h_strip (G,j)) is convex then A2: Int (h_strip (G,j)) = { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 < s & s < (G * (1,(j + 1))) `2 ) } by GOBOARD6:17; A3: { |[r,s]| where r, s is Real : (G * (1,j)) `2 < s } c= the carrier of (TOP-REAL 2) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[r,s]| where r, s is Real : (G * (1,j)) `2 < s } or x in the carrier of (TOP-REAL 2) ) assume x in { |[r,s]| where r, s is Real : (G * (1,j)) `2 < s } ; ::_thesis: x in the carrier of (TOP-REAL 2) then ex r, s being Real st ( x = |[r,s]| & (G * (1,j)) `2 < s ) ; hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum end; { |[r,s]| where r, s is Real : s < (G * (1,(j + 1))) `2 } c= the carrier of (TOP-REAL 2) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[r,s]| where r, s is Real : s < (G * (1,(j + 1))) `2 } or x in the carrier of (TOP-REAL 2) ) assume x in { |[r,s]| where r, s is Real : s < (G * (1,(j + 1))) `2 } ; ::_thesis: x in the carrier of (TOP-REAL 2) then ex r, s being Real st ( x = |[r,s]| & s < (G * (1,(j + 1))) `2 ) ; hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum end; then reconsider P = { |[r,s]| where r, s is Real : (G * (1,j)) `2 < s } , Q = { |[r,s]| where r, s is Real : s < (G * (1,(j + 1))) `2 } as Subset of (TOP-REAL 2) by A3; A4: Int (h_strip (G,j)) = P /\ Q proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: P /\ Q c= Int (h_strip (G,j)) let x be set ; ::_thesis: ( x in Int (h_strip (G,j)) implies x in P /\ Q ) assume x in Int (h_strip (G,j)) ; ::_thesis: x in P /\ Q then A5: ex r, s being Real st ( x = |[r,s]| & (G * (1,j)) `2 < s & s < (G * (1,(j + 1))) `2 ) by A2; then A6: x in P ; x in Q by A5; hence x in P /\ Q by A6, XBOOLE_0:def_4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P /\ Q or x in Int (h_strip (G,j)) ) assume A7: x in P /\ Q ; ::_thesis: x in Int (h_strip (G,j)) then x in P by XBOOLE_0:def_4; then consider r1, s1 being Real such that A8: x = |[r1,s1]| and A9: (G * (1,j)) `2 < s1 ; x in Q by A7, XBOOLE_0:def_4; then consider r2, s2 being Real such that A10: x = |[r2,s2]| and A11: s2 < (G * (1,(j + 1))) `2 ; s1 = s2 by A8, A10, SPPOL_2:1; hence x in Int (h_strip (G,j)) by A2, A8, A9, A11; ::_thesis: verum end; A12: P is convex by JORDAN1:15; Q is convex by JORDAN1:17; hence Int (h_strip (G,j)) is convex by A4, A12, Th6; ::_thesis: verum end; end; end; theorem Th13: :: GOBOARD9:13 for i being Element of NAT for G being Go-board st i <= len G holds Int (v_strip (G,i)) is convex proof let i be Element of NAT ; ::_thesis: for G being Go-board st i <= len G holds Int (v_strip (G,i)) is convex let G be Go-board; ::_thesis: ( i <= len G implies Int (v_strip (G,i)) is convex ) assume A1: i <= len G ; ::_thesis: Int (v_strip (G,i)) is convex percases ( i = 0 or i = len G or ( 1 <= i & i < len G ) ) by A1, NAT_1:14, XXREAL_0:1; suppose i = 0 ; ::_thesis: Int (v_strip (G,i)) is convex then Int (v_strip (G,i)) = { |[r,s]| where r, s is Real : r < (G * (1,1)) `1 } by GOBOARD6:12; hence Int (v_strip (G,i)) is convex by JORDAN1:13; ::_thesis: verum end; suppose i = len G ; ::_thesis: Int (v_strip (G,i)) is convex then Int (v_strip (G,i)) = { |[r,s]| where r, s is Real : (G * ((len G),1)) `1 < r } by GOBOARD6:13; hence Int (v_strip (G,i)) is convex by JORDAN1:11; ::_thesis: verum end; suppose ( 1 <= i & i < len G ) ; ::_thesis: Int (v_strip (G,i)) is convex then A2: Int (v_strip (G,i)) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 < r & r < (G * ((i + 1),1)) `1 ) } by GOBOARD6:14; A3: { |[r,s]| where r, s is Real : (G * (i,1)) `1 < r } c= the carrier of (TOP-REAL 2) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[r,s]| where r, s is Real : (G * (i,1)) `1 < r } or x in the carrier of (TOP-REAL 2) ) assume x in { |[r,s]| where r, s is Real : (G * (i,1)) `1 < r } ; ::_thesis: x in the carrier of (TOP-REAL 2) then ex r, s being Real st ( x = |[r,s]| & (G * (i,1)) `1 < r ) ; hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum end; { |[r,s]| where r, s is Real : r < (G * ((i + 1),1)) `1 } c= the carrier of (TOP-REAL 2) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[r,s]| where r, s is Real : r < (G * ((i + 1),1)) `1 } or x in the carrier of (TOP-REAL 2) ) assume x in { |[r,s]| where r, s is Real : r < (G * ((i + 1),1)) `1 } ; ::_thesis: x in the carrier of (TOP-REAL 2) then ex r, s being Real st ( x = |[r,s]| & r < (G * ((i + 1),1)) `1 ) ; hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum end; then reconsider P = { |[r,s]| where r, s is Real : (G * (i,1)) `1 < r } , Q = { |[r,s]| where r, s is Real : r < (G * ((i + 1),1)) `1 } as Subset of (TOP-REAL 2) by A3; A4: Int (v_strip (G,i)) = P /\ Q proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: P /\ Q c= Int (v_strip (G,i)) let x be set ; ::_thesis: ( x in Int (v_strip (G,i)) implies x in P /\ Q ) assume x in Int (v_strip (G,i)) ; ::_thesis: x in P /\ Q then A5: ex r, s being Real st ( x = |[r,s]| & (G * (i,1)) `1 < r & r < (G * ((i + 1),1)) `1 ) by A2; then A6: x in P ; x in Q by A5; hence x in P /\ Q by A6, XBOOLE_0:def_4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P /\ Q or x in Int (v_strip (G,i)) ) assume A7: x in P /\ Q ; ::_thesis: x in Int (v_strip (G,i)) then x in P by XBOOLE_0:def_4; then consider r1, s1 being Real such that A8: x = |[r1,s1]| and A9: (G * (i,1)) `1 < r1 ; x in Q by A7, XBOOLE_0:def_4; then consider r2, s2 being Real such that A10: x = |[r2,s2]| and A11: r2 < (G * ((i + 1),1)) `1 ; r1 = r2 by A8, A10, SPPOL_2:1; hence x in Int (v_strip (G,i)) by A2, A8, A9, A11; ::_thesis: verum end; A12: P is convex by JORDAN1:11; Q is convex by JORDAN1:13; hence Int (v_strip (G,i)) is convex by A4, A12, Th6; ::_thesis: verum end; end; end; theorem Th14: :: GOBOARD9:14 for i, j being Element of NAT for G being Go-board st i <= len G & j <= width G holds Int (cell (G,i,j)) <> {} proof let i, j be Element of NAT ; ::_thesis: for G being Go-board st i <= len G & j <= width G holds Int (cell (G,i,j)) <> {} let G be Go-board; ::_thesis: ( i <= len G & j <= width G implies Int (cell (G,i,j)) <> {} ) assume that A1: i <= len G and A2: j <= width G ; ::_thesis: Int (cell (G,i,j)) <> {} A3: ( j = width G or j < width G ) by A2, XXREAL_0:1; A4: ( i = len G or i < len G ) by A1, XXREAL_0:1; set p = the Point of (TOP-REAL 2); percases ( ( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G ) or ( 1 <= i & i + 1 <= len G & j = width G ) or ( 1 <= i & i + 1 <= len G & j = 0 ) or ( 1 <= j & j + 1 <= width G & i = 0 ) or ( 1 <= j & j + 1 <= width G & i = len G ) or ( i = 0 & j = 0 ) or ( i = len G & j = width G ) or ( i = 0 & j = width G ) or ( i = len G & j = 0 ) ) by A3, A4, NAT_1:13, NAT_1:14; suppose ( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G ) ; ::_thesis: Int (cell (G,i,j)) <> {} then LSeg (((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))), the Point of (TOP-REAL 2)) meets Int (cell (G,i,j)) by GOBOARD6:82; hence Int (cell (G,i,j)) <> {} by XBOOLE_1:65; ::_thesis: verum end; suppose ( 1 <= i & i + 1 <= len G & j = width G ) ; ::_thesis: Int (cell (G,i,j)) <> {} then LSeg ( the Point of (TOP-REAL 2),(((1 / 2) * ((G * (i,j)) + (G * ((i + 1),j)))) + |[0,1]|)) meets Int (cell (G,i,j)) by GOBOARD6:83; hence Int (cell (G,i,j)) <> {} by XBOOLE_1:65; ::_thesis: verum end; suppose ( 1 <= i & i + 1 <= len G & j = 0 ) ; ::_thesis: Int (cell (G,i,j)) <> {} then LSeg ((((1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 1))))) - |[0,1]|), the Point of (TOP-REAL 2)) meets Int (cell (G,i,j)) by GOBOARD6:84; hence Int (cell (G,i,j)) <> {} by XBOOLE_1:65; ::_thesis: verum end; suppose ( 1 <= j & j + 1 <= width G & i = 0 ) ; ::_thesis: Int (cell (G,i,j)) <> {} then LSeg ((((1 / 2) * ((G * ((i + 1),j)) + (G * ((i + 1),(j + 1))))) - |[1,0]|), the Point of (TOP-REAL 2)) meets Int (cell (G,i,j)) by GOBOARD6:85; hence Int (cell (G,i,j)) <> {} by XBOOLE_1:65; ::_thesis: verum end; suppose ( 1 <= j & j + 1 <= width G & i = len G ) ; ::_thesis: Int (cell (G,i,j)) <> {} then LSeg ( the Point of (TOP-REAL 2),(((1 / 2) * ((G * (i,j)) + (G * (i,(j + 1))))) + |[1,0]|)) meets Int (cell (G,i,j)) by GOBOARD6:86; hence Int (cell (G,i,j)) <> {} by XBOOLE_1:65; ::_thesis: verum end; suppose ( i = 0 & j = 0 ) ; ::_thesis: Int (cell (G,i,j)) <> {} then LSeg ( the Point of (TOP-REAL 2),((G * ((i + 1),(j + 1))) - |[1,1]|)) meets Int (cell (G,i,j)) by GOBOARD6:87; hence Int (cell (G,i,j)) <> {} by XBOOLE_1:65; ::_thesis: verum end; suppose ( i = len G & j = width G ) ; ::_thesis: Int (cell (G,i,j)) <> {} then LSeg ( the Point of (TOP-REAL 2),((G * (i,j)) + |[1,1]|)) meets Int (cell (G,i,j)) by GOBOARD6:88; hence Int (cell (G,i,j)) <> {} by XBOOLE_1:65; ::_thesis: verum end; suppose ( i = 0 & j = width G ) ; ::_thesis: Int (cell (G,i,j)) <> {} then LSeg ( the Point of (TOP-REAL 2),((G * ((i + 1),j)) + |[(- 1),1]|)) meets Int (cell (G,i,j)) by GOBOARD6:89; hence Int (cell (G,i,j)) <> {} by XBOOLE_1:65; ::_thesis: verum end; suppose ( i = len G & j = 0 ) ; ::_thesis: Int (cell (G,i,j)) <> {} then LSeg ( the Point of (TOP-REAL 2),((G * (i,(j + 1))) + |[1,(- 1)]|)) meets Int (cell (G,i,j)) by GOBOARD6:90; hence Int (cell (G,i,j)) <> {} by XBOOLE_1:65; ::_thesis: verum end; end; end; theorem Th15: :: GOBOARD9:15 for f being non constant standard special_circular_sequence for k being Element of NAT st 1 <= k & k + 1 <= len f holds Int (left_cell (f,k)) <> {} proof let f be non constant standard special_circular_sequence; ::_thesis: for k being Element of NAT st 1 <= k & k + 1 <= len f holds Int (left_cell (f,k)) <> {} let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f implies Int (left_cell (f,k)) <> {} ) assume that A1: 1 <= k and A2: k + 1 <= len f ; ::_thesis: Int (left_cell (f,k)) <> {} ex i, j being Element of NAT st ( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) ) by A1, A2, Th11; hence Int (left_cell (f,k)) <> {} by Th14; ::_thesis: verum end; theorem Th16: :: GOBOARD9:16 for f being non constant standard special_circular_sequence for k being Element of NAT st 1 <= k & k + 1 <= len f holds Int (right_cell (f,k)) <> {} proof let f be non constant standard special_circular_sequence; ::_thesis: for k being Element of NAT st 1 <= k & k + 1 <= len f holds Int (right_cell (f,k)) <> {} let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f implies Int (right_cell (f,k)) <> {} ) assume that A1: 1 <= k and A2: k + 1 <= len f ; ::_thesis: Int (right_cell (f,k)) <> {} A3: len f = len (Rev f) by FINSEQ_5:def_3; k <= len f by A2, NAT_1:13; then A4: ((len f) -' k) + k = len f by XREAL_1:235; then A5: ((len f) -' k) + 1 <= len f by A1, XREAL_1:6; A6: (len f) -' k >= 1 by A2, A4, XREAL_1:6; then right_cell (f,k) = left_cell ((Rev f),((len f) -' k)) by A1, A4, Th10; hence Int (right_cell (f,k)) <> {} by A3, A5, A6, Th15; ::_thesis: verum end; theorem Th17: :: GOBOARD9:17 for i, j being Element of NAT for G being Go-board st i <= len G & j <= width G holds Int (cell (G,i,j)) is convex proof let i, j be Element of NAT ; ::_thesis: for G being Go-board st i <= len G & j <= width G holds Int (cell (G,i,j)) is convex let G be Go-board; ::_thesis: ( i <= len G & j <= width G implies Int (cell (G,i,j)) is convex ) assume that A1: i <= len G and A2: j <= width G ; ::_thesis: Int (cell (G,i,j)) is convex set P = Int (cell (G,i,j)); A3: Int (cell (G,i,j)) = (Int (v_strip (G,i))) /\ (Int (h_strip (G,j))) by TOPS_1:17; A4: Int (v_strip (G,i)) is convex by A1, Th13; Int (h_strip (G,j)) is convex by A2, Th12; hence Int (cell (G,i,j)) is convex by A3, A4, Th6; ::_thesis: verum end; theorem :: GOBOARD9:18 canceled; theorem Th19: :: GOBOARD9:19 for f being non constant standard special_circular_sequence for k being Element of NAT st 1 <= k & k + 1 <= len f holds Int (left_cell (f,k)) is convex proof let f be non constant standard special_circular_sequence; ::_thesis: for k being Element of NAT st 1 <= k & k + 1 <= len f holds Int (left_cell (f,k)) is convex let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f implies Int (left_cell (f,k)) is convex ) assume that A1: 1 <= k and A2: k + 1 <= len f ; ::_thesis: Int (left_cell (f,k)) is convex ex i, j being Element of NAT st ( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) ) by A1, A2, Th11; hence Int (left_cell (f,k)) is convex by Th17; ::_thesis: verum end; theorem Th20: :: GOBOARD9:20 for f being non constant standard special_circular_sequence for k being Element of NAT st 1 <= k & k + 1 <= len f holds Int (right_cell (f,k)) is convex proof let f be non constant standard special_circular_sequence; ::_thesis: for k being Element of NAT st 1 <= k & k + 1 <= len f holds Int (right_cell (f,k)) is convex let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f implies Int (right_cell (f,k)) is convex ) assume that A1: 1 <= k and A2: k + 1 <= len f ; ::_thesis: Int (right_cell (f,k)) is convex A3: len f = len (Rev f) by FINSEQ_5:def_3; k <= len f by A2, NAT_1:13; then A4: ((len f) -' k) + k = len f by XREAL_1:235; then A5: ((len f) -' k) + 1 <= len f by A1, XREAL_1:6; A6: (len f) -' k >= 1 by A2, A4, XREAL_1:6; then right_cell (f,k) = left_cell ((Rev f),((len f) -' k)) by A1, A4, Th10; hence Int (right_cell (f,k)) is convex by A3, A5, A6, Th19; ::_thesis: verum end; definition let f be non constant standard special_circular_sequence; A1: 1 + 1 < len f by GOBOARD7:34, XXREAL_0:2; then A2: Int (left_cell (f,1)) <> {} by Th15; A3: Int (right_cell (f,1)) <> {} by A1, Th16; func LeftComp f -> Subset of (TOP-REAL 2) means :Def1: :: GOBOARD9:def 1 ( it is_a_component_of (L~ f) ` & Int (left_cell (f,1)) c= it ); existence ex b1 being Subset of (TOP-REAL 2) st ( b1 is_a_component_of (L~ f) ` & Int (left_cell (f,1)) c= b1 ) proof A4: Int (left_cell (f,1)) is convex by A1, Th19; Int (left_cell (f,1)) misses L~ f by A1, GOBOARD8:37; then A5: Int (left_cell (f,1)) c= (L~ f) ` by SUBSET_1:23; then (L~ f) ` <> {} by A1, Th15, XBOOLE_1:3; hence ex b1 being Subset of (TOP-REAL 2) st ( b1 is_a_component_of (L~ f) ` & Int (left_cell (f,1)) c= b1 ) by A2, A4, A5, Th3; ::_thesis: verum end; uniqueness for b1, b2 being Subset of (TOP-REAL 2) st b1 is_a_component_of (L~ f) ` & Int (left_cell (f,1)) c= b1 & b2 is_a_component_of (L~ f) ` & Int (left_cell (f,1)) c= b2 holds b1 = b2 by A2, Th1, XBOOLE_1:67; func RightComp f -> Subset of (TOP-REAL 2) means :Def2: :: GOBOARD9:def 2 ( it is_a_component_of (L~ f) ` & Int (right_cell (f,1)) c= it ); existence ex b1 being Subset of (TOP-REAL 2) st ( b1 is_a_component_of (L~ f) ` & Int (right_cell (f,1)) c= b1 ) proof A6: Int (right_cell (f,1)) is convex by A1, Th20; Int (right_cell (f,1)) misses L~ f by A1, GOBOARD8:38; then A7: Int (right_cell (f,1)) c= (L~ f) ` by SUBSET_1:23; then (L~ f) ` <> {} by A1, Th16, XBOOLE_1:3; hence ex b1 being Subset of (TOP-REAL 2) st ( b1 is_a_component_of (L~ f) ` & Int (right_cell (f,1)) c= b1 ) by A3, A6, A7, Th3; ::_thesis: verum end; uniqueness for b1, b2 being Subset of (TOP-REAL 2) st b1 is_a_component_of (L~ f) ` & Int (right_cell (f,1)) c= b1 & b2 is_a_component_of (L~ f) ` & Int (right_cell (f,1)) c= b2 holds b1 = b2 by A3, Th1, XBOOLE_1:67; end; :: deftheorem Def1 defines LeftComp GOBOARD9:def_1_:_ for f being non constant standard special_circular_sequence for b2 being Subset of (TOP-REAL 2) holds ( b2 = LeftComp f iff ( b2 is_a_component_of (L~ f) ` & Int (left_cell (f,1)) c= b2 ) ); :: deftheorem Def2 defines RightComp GOBOARD9:def_2_:_ for f being non constant standard special_circular_sequence for b2 being Subset of (TOP-REAL 2) holds ( b2 = RightComp f iff ( b2 is_a_component_of (L~ f) ` & Int (right_cell (f,1)) c= b2 ) ); theorem Th21: :: GOBOARD9:21 for f being non constant standard special_circular_sequence for k being Element of NAT st 1 <= k & k + 1 <= len f holds Int (left_cell (f,k)) c= LeftComp f proof let f be non constant standard special_circular_sequence; ::_thesis: for k being Element of NAT st 1 <= k & k + 1 <= len f holds Int (left_cell (f,k)) c= LeftComp f defpred S1[ Element of NAT ] means ( 1 <= \$1 & \$1 + 1 <= len f implies Int (left_cell (f,\$1)) c= LeftComp f ); A1: S1[ 0 ] ; A2: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: S1[k] ; ::_thesis: S1[k + 1] thus S1[k + 1] ::_thesis: verum proof assume that A4: 1 <= k + 1 and A5: (k + 1) + 1 <= len f ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f percases ( k = 0 or k >= 1 ) by NAT_1:14; suppose k = 0 ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f hence Int (left_cell (f,(k + 1))) c= LeftComp f by Def1; ::_thesis: verum end; supposeA6: k >= 1 ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f A7: k + 1 <= len f by A5, NAT_1:13; A8: k <= k + 1 by NAT_1:11; then k <= len f by A7, XXREAL_0:2; then A9: k in dom f by A6, FINSEQ_3:25; then consider i0, j0 being Element of NAT such that A10: [i0,j0] in Indices (GoB f) and A11: f /. k = (GoB f) * (i0,j0) by GOBOARD2:14; A12: k + 1 in dom f by A4, A7, FINSEQ_3:25; then consider i1, j1 being Element of NAT such that A13: [i1,j1] in Indices (GoB f) and A14: f /. (k + 1) = (GoB f) * (i1,j1) by GOBOARD2:14; (k + 1) + 1 >= 1 by NAT_1:11; then A15: (k + 1) + 1 in dom f by A5, FINSEQ_3:25; then consider i2, j2 being Element of NAT such that A16: [i2,j2] in Indices (GoB f) and A17: f /. ((k + 1) + 1) = (GoB f) * (i2,j2) by GOBOARD2:14; A18: 1 <= i0 by A10, MATRIX_1:38; A19: i0 <= len (GoB f) by A10, MATRIX_1:38; A20: 1 <= i1 by A13, MATRIX_1:38; A21: i1 <= len (GoB f) by A13, MATRIX_1:38; A22: 1 <= i2 by A16, MATRIX_1:38; A23: i2 <= len (GoB f) by A16, MATRIX_1:38; A24: 1 <= j0 by A10, MATRIX_1:38; A25: j0 <= width (GoB f) by A10, MATRIX_1:38; A26: 1 <= j1 by A13, MATRIX_1:38; A27: j1 <= width (GoB f) by A13, MATRIX_1:38; A28: 1 <= j2 by A16, MATRIX_1:38; A29: j2 <= width (GoB f) by A16, MATRIX_1:38; A30: ( i0 = i1 or j0 = j1 ) by A9, A10, A11, A12, A13, A14, GOBOARD2:11; A31: ( i1 = i2 or j1 = j2 ) by A12, A13, A14, A15, A16, A17, GOBOARD2:11; reconsider i19 = i1, i09 = i0, i29 = i2, j19 = j1, j09 = j0, j29 = j2 as Element of REAL ; A32: f is_sequence_on GoB f by GOBOARD5:def_5; then (abs (i0 - i1)) + (abs (j0 - j1)) = 1 by A9, A10, A11, A12, A13, A14, GOBOARD1:def_9; then A33: ( ( abs (i09 - i19) = 1 & j0 = j1 ) or ( abs (j09 - j19) = 1 & i0 = i1 ) ) by SEQM_3:42; then A34: ( i0 = i1 or i0 = i1 + 1 or i0 + 1 = i1 ) by SEQM_3:41; (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A12, A13, A14, A15, A16, A17, A32, GOBOARD1:def_9; then A35: ( ( abs (i19 - i29) = 1 & j1 = j2 ) or ( abs (j19 - j29) = 1 & i1 = i2 ) ) by SEQM_3:42; then A36: ( i1 = i2 or i1 = i2 + 1 or i1 + 1 = i2 ) by SEQM_3:41; A37: ( j0 = j1 or j0 = j1 + 1 or j0 + 1 = j1 ) by A33, SEQM_3:41; A38: ( j1 = j2 or j1 = j2 + 1 or j1 + 1 = j2 ) by A35, SEQM_3:41; A39: now__::_thesis:_(_i0_=_i2_implies_not_j0_=_j2_) assume that A40: i0 = i2 and A41: j0 = j2 ; ::_thesis: contradiction A42: now__::_thesis:_(_k_<=_1_implies_not_(k_+_1)_+_1_>=_len_f_) assume k <= 1 ; ::_thesis: not (k + 1) + 1 >= len f then A43: k = 1 by A6, XXREAL_0:1; assume (k + 1) + 1 >= len f ; ::_thesis: contradiction then (k + 1) + 1 = len f by A5, XXREAL_0:1; hence contradiction by A43, GOBOARD7:34; ::_thesis: verum end; A44: k < (k + 1) + 1 by A8, NAT_1:13; percases ( k > 1 or (k + 1) + 1 < len f ) by A42; suppose k > 1 ; ::_thesis: contradiction hence contradiction by A5, A11, A17, A40, A41, A44, GOBOARD7:37; ::_thesis: verum end; suppose (k + 1) + 1 < len f ; ::_thesis: contradiction hence contradiction by A6, A11, A17, A40, A41, A44, GOBOARD7:36; ::_thesis: verum end; end; end; i1 >= 1 by A13, MATRIX_1:38; then A45: i1 = (i1 -' 1) + 1 by XREAL_1:235; j1 >= 1 by A13, MATRIX_1:38; then A46: j1 = (j1 -' 1) + 1 by XREAL_1:235; then j1 -' 1 <= j1 by NAT_1:11; then A47: j1 -' 1 <= width (GoB f) by A27, XXREAL_0:2; len (GoB f) > 1 by GOBOARD7:32; then A48: ((len (GoB f)) -' 1) + 1 = len (GoB f) by XREAL_1:235; width (GoB f) >= 1 by GOBOARD7:33; then A49: ((width (GoB f)) -' 1) + 1 = width (GoB f) by XREAL_1:235; A50: (k + 1) + 1 = k + (1 + 1) ; A51: (i0 + 1) + 1 = i0 + (1 + 1) ; A52: (i2 + 1) + 1 = i2 + (1 + 1) ; A53: (j0 + 1) + 1 = j0 + (1 + 1) ; A54: (j2 + 1) + 1 = j2 + (1 + 1) ; A55: LeftComp f is_a_component_of (L~ f) ` by Def1; A56: 0 + 1 = 1 ; now__::_thesis:_Int_(left_cell_(f,(k_+_1)))_c=_LeftComp_f percases ( ( i0 = i1 + 1 & i1 = i2 + 1 & j0 = 1 ) or ( i0 = i1 + 1 & i1 = i2 + 1 & j0 <> 1 ) or ( i0 = i1 + 1 & j1 = j2 + 1 ) or ( j0 = j1 + 1 & i1 = i2 + 1 & i0 = len (GoB f) & j1 = 1 ) or ( j0 = j1 + 1 & i1 = i2 + 1 & i0 <> len (GoB f) & j1 = 1 ) or ( j0 = j1 + 1 & i1 = i2 + 1 & i0 = len (GoB f) & j1 <> 1 ) or ( j0 = j1 + 1 & i1 = i2 + 1 & i0 <> len (GoB f) & j1 <> 1 ) or ( j0 = j1 + 1 & j1 = j2 + 1 & i0 = len (GoB f) ) or ( j0 = j1 + 1 & j1 = j2 + 1 & i0 <> len (GoB f) ) or ( i0 + 1 = i1 & j1 = j2 + 1 & i1 = len (GoB f) & j0 = width (GoB f) ) or ( i0 + 1 = i1 & j1 = j2 + 1 & i1 <> len (GoB f) & j0 = width (GoB f) ) or ( i0 + 1 = i1 & j1 = j2 + 1 & i1 = len (GoB f) & j0 <> width (GoB f) ) or ( i0 + 1 = i1 & j1 = j2 + 1 & i1 <> len (GoB f) & j0 <> width (GoB f) ) or ( j0 + 1 = j1 & i1 = i2 + 1 ) or ( i0 = i1 + 1 & j1 + 1 = j2 & i1 = 1 & j1 = 1 ) or ( i0 = i1 + 1 & j1 + 1 = j2 & i1 <> 1 & j1 = 1 ) or ( i0 = i1 + 1 & j1 + 1 = j2 & i1 = 1 & j1 <> 1 ) or ( i0 = i1 + 1 & j1 + 1 = j2 & i1 <> 1 & j1 <> 1 ) or ( j0 = j1 + 1 & i1 + 1 = i2 ) or ( i0 + 1 = i1 & i1 + 1 = i2 & j0 = width (GoB f) ) or ( i0 + 1 = i1 & i1 + 1 = i2 & j0 <> width (GoB f) ) or ( i0 + 1 = i1 & j1 + 1 = j2 ) or ( j0 + 1 = j1 & i1 + 1 = i2 & i0 = 1 & j1 = width (GoB f) ) or ( j0 + 1 = j1 & i1 + 1 = i2 & i0 <> 1 & j1 = width (GoB f) ) or ( j0 + 1 = j1 & i1 + 1 = i2 & i0 = 1 & j1 <> width (GoB f) ) or ( j0 + 1 = j1 & i1 + 1 = i2 & i0 <> 1 & j1 <> width (GoB f) ) or ( j0 + 1 = j1 & j1 + 1 = j2 & i0 = 1 ) or ( j0 + 1 = j1 & j1 + 1 = j2 & i0 <> 1 ) ) by A9, A11, A12, A14, A15, A17, A34, A36, A37, A38, A39, GOBOARD7:29; supposethat A57: i0 = i1 + 1 and A58: i1 = i2 + 1 and A59: j0 = 1 ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f A60: left_cell (f,k) = cell ((GoB f),i1,0) by A6, A7, A10, A11, A13, A14, A30, A56, A57, A59, GOBOARD5:29; 0 + 1 = j2 by A30, A31, A57, A58, A59; then A61: left_cell (f,(k + 1)) = cell ((GoB f),i2,0) by A4, A5, A13, A14, A16, A17, A30, A57, A58, A59, GOBOARD5:29; A62: LSeg ((((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * (i0,1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * (i2,1)) + ((GoB f) * (i1,1)))) - |[0,1]|)) meets Int (cell ((GoB f),i1,0)) by A19, A20, A57, GOBOARD6:84; LSeg ((((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * (i0,1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * (i2,1)) + ((GoB f) * (i1,1)))) - |[0,1]|)) misses L~ f by A19, A22, A52, A57, A58, GOBOARD8:25; then LSeg ((((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * (i0,1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * (i2,1)) + ((GoB f) * (i1,1)))) - |[0,1]|)) c= (L~ f) ` by SUBSET_1:23; then A63: LSeg ((((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * (i0,1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * (i2,1)) + ((GoB f) * (i1,1)))) - |[0,1]|)) c= LeftComp f by A3, A5, A6, A55, A60, A62, Th4, NAT_1:13; A64: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19; Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37; then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23; hence Int (left_cell (f,(k + 1))) c= LeftComp f by A55, A61, A63, A21, A22, A58, GOBOARD6:84, Th4, A64; ::_thesis: verum end; supposethat A65: i0 = i1 + 1 and A66: i1 = i2 + 1 and A67: j0 <> 1 ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f A68: left_cell (f,k) = cell ((GoB f),i1,(j1 -' 1)) by A6, A7, A10, A11, A13, A14, A30, A46, A65, GOBOARD5:29; 1 < j0 by A24, A67, XXREAL_0:1; then A69: 1 <= j0 -' 1 by A30, A46, A65, NAT_1:13; A70: left_cell (f,(k + 1)) = cell ((GoB f),i2,(j1 -' 1)) by A4, A5, A13, A14, A16, A17, A31, A46, A66, GOBOARD5:29; A71: LSeg (((1 / 2) * (((GoB f) * (i1,(j0 -' 1))) + ((GoB f) * (i0,j0)))),((1 / 2) * (((GoB f) * (i2,(j0 -' 1))) + ((GoB f) * (i1,j0))))) meets Int (cell ((GoB f),i1,(j1 -' 1))) by A19, A20, A27, A30, A46, A65, A69, GOBOARD6:82; LSeg (((1 / 2) * (((GoB f) * (i1,(j0 -' 1))) + ((GoB f) * (i0,j0)))),((1 / 2) * (((GoB f) * (i2,(j0 -' 1))) + ((GoB f) * (i1,j0))))) misses L~ f by A5, A6, A11, A14, A17, A19, A22, A25, A30, A31, A46, A50, A52, A65, A66, A69, GOBOARD8:11; then LSeg (((1 / 2) * (((GoB f) * (i1,(j0 -' 1))) + ((GoB f) * (i0,j0)))),((1 / 2) * (((GoB f) * (i2,(j0 -' 1))) + ((GoB f) * (i1,j0))))) c= (L~ f) ` by SUBSET_1:23; then A72: LSeg (((1 / 2) * (((GoB f) * (i1,(j0 -' 1))) + ((GoB f) * (i0,j0)))),((1 / 2) * (((GoB f) * (i2,(j0 -' 1))) + ((GoB f) * (i1,j0))))) c= LeftComp f by A3, A5, A6, A55, A68, A71, Th4, NAT_1:13; A73: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19; Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37; then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23; hence Int (left_cell (f,(k + 1))) c= LeftComp f by A30, A55, A65, A66, A70, A72, A21, A22, A25, A46, A69, GOBOARD6:82, Th4, A73; ::_thesis: verum end; supposethat A74: i0 = i1 + 1 and A75: j1 = j2 + 1 ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f left_cell (f,k) = cell ((GoB f),i1,j2) by A6, A7, A10, A11, A13, A14, A30, A74, A75, GOBOARD5:29 .= left_cell (f,(k + 1)) by A4, A5, A13, A14, A16, A17, A31, A45, A75, GOBOARD5:30 ; hence Int (left_cell (f,(k + 1))) c= LeftComp f by A3, A5, A6, NAT_1:13; ::_thesis: verum end; supposethat A76: j0 = j1 + 1 and A77: i1 = i2 + 1 and A78: i0 = len (GoB f) and A79: j1 = 1 ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f A80: left_cell (f,k) = cell ((GoB f),i0,j1) by A6, A7, A10, A11, A13, A14, A30, A45, A76, GOBOARD5:30; A81: LSeg ((((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),1)) + ((GoB f) * ((len (GoB f)),2)))) + |[1,0]|)) meets Int (cell ((GoB f),i0,j1)) by A25, A76, A78, A79, GOBOARD6:86; LSeg ((((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),1)) + ((GoB f) * ((len (GoB f)),2)))) + |[1,0]|)) misses L~ f by GOBOARD8:35; then LSeg ((((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),1)) + ((GoB f) * ((len (GoB f)),2)))) + |[1,0]|)) c= (L~ f) ` by SUBSET_1:23; then A82: LSeg ((((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),1)) + ((GoB f) * ((len (GoB f)),2)))) + |[1,0]|)) c= LeftComp f by A3, A5, A6, A55, A80, A81, Th4, NAT_1:13; A83: Int (cell ((GoB f),i1,0)) is convex by A21, A26, A27, Th17; Int (cell ((GoB f),i1,0)) misses L~ f by A21, A26, A27, GOBOARD7:12; then Int (cell ((GoB f),i1,0)) c= (L~ f) ` by SUBSET_1:23; then A84: Int (cell ((GoB f),i1,0)) c= LeftComp f by A55, A82, A30, A76, A78, GOBOARD6:90, Th4, A83; A85: left_cell (f,(k + 1)) = cell ((GoB f),i2,0) by A4, A5, A13, A14, A16, A17, A31, A46, A77, A79, GOBOARD5:29; A86: LSeg ((((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1)))) - |[0,1]|),(((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|)) meets Int (cell ((GoB f),i1,0)) by A30, A76, A78, GOBOARD6:90; LSeg ((((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1)))) - |[0,1]|),(((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|)) misses L~ f by GOBOARD8:27; then LSeg ((((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1)))) - |[0,1]|),(((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|)) c= (L~ f) ` by SUBSET_1:23; then A87: LSeg ((((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1)))) - |[0,1]|),(((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|)) c= LeftComp f by A55, A84, A86, Th4; A88: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19; Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37; then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23; hence Int (left_cell (f,(k + 1))) c= LeftComp f by A55, A85, A87, A22, A30, A45, A76, A77, A78, GOBOARD6:84, Th4, A88; ::_thesis: verum end; supposethat A89: j0 = j1 + 1 and A90: i1 = i2 + 1 and A91: i0 <> len (GoB f) and A92: j1 = 1 ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f A93: left_cell (f,k) = cell ((GoB f),i0,j1) by A6, A7, A10, A11, A13, A14, A30, A45, A89, GOBOARD5:30; len (GoB f) > i0 by A19, A91, XXREAL_0:1; then A94: len (GoB f) >= i0 + 1 by NAT_1:13; A95: LSeg ((((1 / 2) * (((GoB f) * (i0,1)) + ((GoB f) * ((i0 + 1),1)))) - |[0,1]|),((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * ((i1 + 1),(1 + 1)))))) meets Int (cell ((GoB f),i0,j1)) by A20, A25, A30, A89, A92, A94, GOBOARD6:82; LSeg ((((1 / 2) * (((GoB f) * (i0,1)) + ((GoB f) * ((i0 + 1),1)))) - |[0,1]|),((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * ((i1 + 1),2))))) misses L~ f by A5, A6, A11, A14, A17, A22, A30, A31, A50, A52, A89, A90, A92, A94, GOBOARD8:8; then LSeg ((((1 / 2) * (((GoB f) * (i0,1)) + ((GoB f) * ((i0 + 1),1)))) - |[0,1]|),((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * ((i1 + 1),2))))) c= (L~ f) ` by SUBSET_1:23; then A96: LSeg ((((1 / 2) * (((GoB f) * (i0,1)) + ((GoB f) * ((i0 + 1),1)))) - |[0,1]|),((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * ((i1 + 1),2))))) c= LeftComp f by A3, A5, A6, A55, A93, A95, Th4, NAT_1:13; A97: Int (cell ((GoB f),i1,0)) is convex by A21, A26, A27, Th17; Int (cell ((GoB f),i1,0)) misses L~ f by A21, A26, A27, GOBOARD7:12; then Int (cell ((GoB f),i1,0)) c= (L~ f) ` by SUBSET_1:23; then A98: Int (cell ((GoB f),i1,0)) c= LeftComp f by A55, A96, A20, A30, A89, A94, GOBOARD6:84, Th4, A97; A99: left_cell (f,(k + 1)) = cell ((GoB f),i2,0) by A4, A5, A13, A14, A16, A17, A31, A46, A90, A92, GOBOARD5:29; A100: LSeg ((((1 / 2) * (((GoB f) * (i2,1)) + ((GoB f) * ((i2 + 1),1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * ((i2 + 1),1)) + ((GoB f) * ((i2 + 2),1)))) - |[0,1]|)) meets Int (cell ((GoB f),i1,0)) by A20, A30, A89, A90, A94, GOBOARD6:84; LSeg ((((1 / 2) * (((GoB f) * (i2,1)) + ((GoB f) * ((i2 + 1),1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * ((i2 + 1),1)) + ((GoB f) * ((i2 + 2),1)))) - |[0,1]|)) misses L~ f by A22, A30, A89, A90, A94, GOBOARD8:25; then LSeg ((((1 / 2) * (((GoB f) * (i2,1)) + ((GoB f) * ((i2 + 1),1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * ((i2 + 1),1)) + ((GoB f) * ((i2 + 2),1)))) - |[0,1]|)) c= (L~ f) ` by SUBSET_1:23; then A101: LSeg ((((1 / 2) * (((GoB f) * (i2,1)) + ((GoB f) * ((i2 + 1),1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * ((i2 + 1),1)) + ((GoB f) * ((i2 + 2),1)))) - |[0,1]|)) c= LeftComp f by A55, A98, A100, Th4; A102: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19; Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37; then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23; hence Int (left_cell (f,(k + 1))) c= LeftComp f by A55, A99, A101, A21, A22, A90, GOBOARD6:84, Th4, A102; ::_thesis: verum end; supposethat A103: j0 = j1 + 1 and A104: i1 = i2 + 1 and A105: i0 = len (GoB f) and A106: j1 <> 1 ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f A107: left_cell (f,k) = cell ((GoB f),i0,j1) by A6, A7, A10, A11, A13, A14, A30, A45, A103, GOBOARD5:30; 1 < j1 by A26, A106, XXREAL_0:1; then A108: 1 <= j1 -' 1 by A46, NAT_1:13; A109: j1 + 1 = (j1 -' 1) + (1 + 1) by A46; A110: LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),(j1 -' 1))) + ((GoB f) * ((len (GoB f)),j1)))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1))))) + |[1,0]|)) meets Int (cell ((GoB f),i0,j1)) by A25, A26, A103, A105, GOBOARD6:86; LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),(j1 -' 1))) + ((GoB f) * ((len (GoB f)),j1)))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1))))) + |[1,0]|)) misses L~ f by A25, A46, A103, A108, A109, GOBOARD8:34; then LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),(j1 -' 1))) + ((GoB f) * ((len (GoB f)),j1)))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1))))) + |[1,0]|)) c= (L~ f) ` by SUBSET_1:23; then A111: LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),(j1 -' 1))) + ((GoB f) * ((len (GoB f)),j1)))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1))))) + |[1,0]|)) c= LeftComp f by A3, A5, A6, A55, A107, A110, Th4, NAT_1:13; j1 > 1 by A26, A106, XXREAL_0:1; then A112: 1 <= j1 -' 1 by A46, NAT_1:13; A113: Int (cell ((GoB f),i1,(j1 -' 1))) is convex by A21, A47, Th17; Int (cell ((GoB f),i1,(j1 -' 1))) misses L~ f by A21, A47, GOBOARD7:12; then Int (cell ((GoB f),i1,(j1 -' 1))) c= (L~ f) ` by SUBSET_1:23; then A114: Int (cell ((GoB f),i1,(j1 -' 1))) c= LeftComp f by A55, A111, A27, A30, A46, A103, A105, GOBOARD6:86, Th4, A113, A112; A115: left_cell (f,(k + 1)) = cell ((GoB f),i2,(j1 -' 1)) by A4, A5, A13, A14, A16, A17, A31, A46, A104, GOBOARD5:29; A116: LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),(j1 -' 1))) + ((GoB f) * (i1,j1)))),(((1 / 2) * (((GoB f) * (i1,(j1 -' 1))) + ((GoB f) * (i1,j1)))) + |[1,0]|)) meets Int (cell ((GoB f),i1,(j1 -' 1))) by A27, A30, A46, A103, A105, A108, GOBOARD6:86; A117: i1 -' 1 = i2 by A104, NAT_D:34; then LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),(j1 -' 1))) + ((GoB f) * (i1,j1)))),(((1 / 2) * (((GoB f) * (i1,(j1 -' 1))) + ((GoB f) * (i1,j1)))) + |[1,0]|)) misses L~ f by A5, A6, A11, A14, A17, A25, A30, A31, A46, A50, A103, A104, A105, A108, A109, GOBOARD8:19; then LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),(j1 -' 1))) + ((GoB f) * (i1,j1)))),(((1 / 2) * (((GoB f) * (i1,(j1 -' 1))) + ((GoB f) * (i1,j1)))) + |[1,0]|)) c= (L~ f) ` by SUBSET_1:23; then A118: LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),(j1 -' 1))) + ((GoB f) * (i1,j1)))),(((1 / 2) * (((GoB f) * (i1,(j1 -' 1))) + ((GoB f) * (i1,j1)))) + |[1,0]|)) c= LeftComp f by A55, A114, A116, Th4; A119: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19; Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37; then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23; hence Int (left_cell (f,(k + 1))) c= LeftComp f by A55, A115, A118, A21, A22, A27, A46, A104, A108, A117, GOBOARD6:82, Th4, A119; ::_thesis: verum end; supposethat A120: j0 = j1 + 1 and A121: i1 = i2 + 1 and A122: i0 <> len (GoB f) and A123: j1 <> 1 ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f A124: left_cell (f,k) = cell ((GoB f),i0,j1) by A6, A7, A10, A11, A13, A14, A30, A45, A120, GOBOARD5:30; 1 < j1 by A26, A123, XXREAL_0:1; then A125: 1 <= j1 -' 1 by A46, NAT_1:13; len (GoB f) > i0 by A19, A122, XXREAL_0:1; then A126: len (GoB f) >= i0 + 1 by NAT_1:13; A127: j1 + 1 = (j1 -' 1) + (1 + 1) by A46; A128: LSeg (((1 / 2) * (((GoB f) * (i0,(j1 -' 1))) + ((GoB f) * ((i0 + 1),j1)))),((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * ((i1 + 1),(j1 + 1)))))) meets Int (cell ((GoB f),i0,j1)) by A20, A25, A26, A30, A120, A126, GOBOARD6:82; LSeg (((1 / 2) * (((GoB f) * (i0,(j1 -' 1))) + ((GoB f) * ((i0 + 1),j1)))),((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * ((i1 + 1),(j1 + 1)))))) misses L~ f by A5, A6, A11, A14, A17, A22, A25, A30, A31, A46, A50, A52, A120, A121, A125, A126, A127, GOBOARD8:5; then LSeg (((1 / 2) * (((GoB f) * (i0,(j1 -' 1))) + ((GoB f) * ((i0 + 1),j1)))),((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * ((i1 + 1),(j1 + 1)))))) c= (L~ f) ` by SUBSET_1:23; then A129: LSeg (((1 / 2) * (((GoB f) * (i0,(j1 -' 1))) + ((GoB f) * ((i0 + 1),j1)))),((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * ((i1 + 1),(j1 + 1)))))) c= LeftComp f by A3, A5, A6, A55, A124, A128, Th4, NAT_1:13; j1 > 1 by A26, A123, XXREAL_0:1; then A130: 1 <= j1 -' 1 by A46, NAT_1:13; A131: Int (cell ((GoB f),i1,(j1 -' 1))) is convex by A21, A47, Th17; Int (cell ((GoB f),i1,(j1 -' 1))) misses L~ f by A21, A47, GOBOARD7:12; then Int (cell ((GoB f),i1,(j1 -' 1))) c= (L~ f) ` by SUBSET_1:23; then A132: Int (cell ((GoB f),i1,(j1 -' 1))) c= LeftComp f by A30, A55, A120, A129, A20, A27, A46, A126, GOBOARD6:82, Th4, A131, A130; A133: left_cell (f,(k + 1)) = cell ((GoB f),i2,(j1 -' 1)) by A4, A5, A13, A14, A16, A17, A31, A46, A121, GOBOARD5:29; A134: LSeg (((1 / 2) * (((GoB f) * (i1,(j1 -' 1))) + ((GoB f) * ((i1 + 1),j1)))),((1 / 2) * (((GoB f) * (i2,(j1 -' 1))) + ((GoB f) * (i1,j1))))) meets Int (cell ((GoB f),i1,(j1 -' 1))) by A20, A27, A30, A46, A120, A125, A126, GOBOARD6:82; i1 < len (GoB f) by A21, A30, A120, A122, XXREAL_0:1; then i1 + 1 <= len (GoB f) by NAT_1:13; then LSeg (((1 / 2) * (((GoB f) * (i1,(j1 -' 1))) + ((GoB f) * ((i1 + 1),j1)))),((1 / 2) * (((GoB f) * (i2,(j1 -' 1))) + ((GoB f) * (i1,j1))))) misses L~ f by A5, A6, A11, A14, A17, A22, A25, A30, A31, A46, A50, A52, A120, A121, A125, A127, GOBOARD8:13; then LSeg (((1 / 2) * (((GoB f) * (i1,(j1 -' 1))) + ((GoB f) * ((i1 + 1),j1)))),((1 / 2) * (((GoB f) * (i2,(j1 -' 1))) + ((GoB f) * (i1,j1))))) c= (L~ f) ` by SUBSET_1:23; then A135: LSeg (((1 / 2) * (((GoB f) * (i1,(j1 -' 1))) + ((GoB f) * ((i1 + 1),j1)))),((1 / 2) * (((GoB f) * (i2,(j1 -' 1))) + ((GoB f) * (i1,j1))))) c= LeftComp f by A55, A132, A134, Th4; A136: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19; Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37; then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23; hence Int (left_cell (f,(k + 1))) c= LeftComp f by A55, A121, A133, A135, A21, A22, A27, A46, A125, GOBOARD6:82, Th4, A136; ::_thesis: verum end; supposethat A137: j0 = j1 + 1 and A138: j1 = j2 + 1 and A139: i0 = len (GoB f) ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f A140: left_cell (f,k) = cell ((GoB f),(len (GoB f)),j1) by A6, A7, A10, A11, A13, A14, A30, A48, A137, A139, GOBOARD5:30; A141: left_cell (f,(k + 1)) = cell ((GoB f),(len (GoB f)),j2) by A4, A5, A13, A14, A16, A17, A30, A31, A48, A137, A138, A139, GOBOARD5:30; A142: LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),(j2 + 1))))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),(j2 + 1))) + ((GoB f) * ((len (GoB f)),(j2 + 2))))) + |[1,0]|)) meets Int (cell ((GoB f),(len (GoB f)),j1)) by A25, A26, A137, A138, GOBOARD6:86; LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),(j2 + 1))))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),(j2 + 1))) + ((GoB f) * ((len (GoB f)),(j2 + 2))))) + |[1,0]|)) misses L~ f by A25, A28, A137, A138, GOBOARD8:34; then LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),(j2 + 1))))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),(j2 + 1))) + ((GoB f) * ((len (GoB f)),(j2 + 2))))) + |[1,0]|)) c= (L~ f) ` by SUBSET_1:23; then A143: LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),(j2 + 1))))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),(j2 + 1))) + ((GoB f) * ((len (GoB f)),(j2 + 2))))) + |[1,0]|)) c= LeftComp f by A3, A5, A6, A55, A140, A142, Th4, NAT_1:13; A144: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19; Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37; then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23; hence Int (left_cell (f,(k + 1))) c= LeftComp f by A55, A141, A143, A27, A28, A138, GOBOARD6:86, Th4, A144; ::_thesis: verum end; supposethat A145: j0 = j1 + 1 and A146: j1 = j2 + 1 and A147: i0 <> len (GoB f) ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f A148: left_cell (f,k) = cell ((GoB f),i0,j1) by A6, A7, A10, A11, A13, A14, A30, A45, A145, GOBOARD5:30; len (GoB f) > i0 by A19, A147, XXREAL_0:1; then A149: len (GoB f) >= i0 + 1 by NAT_1:13; A150: left_cell (f,(k + 1)) = cell ((GoB f),i1,j2) by A4, A5, A13, A14, A16, A17, A31, A45, A146, GOBOARD5:30; A151: LSeg (((1 / 2) * (((GoB f) * (i0,j2)) + ((GoB f) * ((i0 + 1),(j2 + 1))))),((1 / 2) * (((GoB f) * (i1,(j2 + 1))) + ((GoB f) * ((i1 + 1),(j2 + 2)))))) meets Int (cell ((GoB f),i0,j1)) by A20, A25, A26, A30, A145, A146, A149, GOBOARD6:82; LSeg (((1 / 2) * (((GoB f) * (i0,j2)) + ((GoB f) * ((i0 + 1),(j2 + 1))))),((1 / 2) * (((GoB f) * (i1,(j2 + 1))) + ((GoB f) * ((i1 + 1),(j2 + 2)))))) misses L~ f by A5, A6, A11, A14, A17, A18, A25, A28, A30, A31, A50, A145, A146, A149, GOBOARD8:4; then LSeg (((1 / 2) * (((GoB f) * (i0,j2)) + ((GoB f) * ((i0 + 1),(j2 + 1))))),((1 / 2) * (((GoB f) * (i1,(j2 + 1))) + ((GoB f) * ((i1 + 1),(j2 + 2)))))) c= (L~ f) ` by SUBSET_1:23; then A152: LSeg (((1 / 2) * (((GoB f) * (i0,j2)) + ((GoB f) * ((i0 + 1),(j2 + 1))))),((1 / 2) * (((GoB f) * (i1,(j2 + 1))) + ((GoB f) * ((i1 + 1),(j2 + 2)))))) c= LeftComp f by A3, A5, A6, A55, A148, A151, Th4, NAT_1:13; A153: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19; Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37; then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23; hence Int (left_cell (f,(k + 1))) c= LeftComp f by A55, A150, A152, A20, A27, A28, A30, A145, A146, A149, GOBOARD6:82, Th4, A153; ::_thesis: verum end; supposethat A154: i0 + 1 = i1 and A155: j1 = j2 + 1 and A156: i1 = len (GoB f) and A157: j0 = width (GoB f) ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f A158: left_cell (f,k) = cell ((GoB f),i0,j1) by A6, A7, A10, A11, A13, A14, A30, A46, A154, GOBOARD5:28; A159: LSeg ((((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * (i1,j0)))) + |[0,1]|),(((GoB f) * (i1,j0)) + |[1,1]|)) meets Int (cell ((GoB f),i0,j1)) by A18, A21, A30, A154, A157, GOBOARD6:83; LSeg ((((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * (i1,j0)))) + |[0,1]|),(((GoB f) * (i1,j0)) + |[1,1]|)) misses L~ f by A48, A154, A156, A157, GOBOARD8:30; then LSeg ((((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * (i1,j0)))) + |[0,1]|),(((GoB f) * (i1,j0)) + |[1,1]|)) c= (L~ f) ` by SUBSET_1:23; then A160: LSeg ((((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * (i1,j0)))) + |[0,1]|),(((GoB f) * (i1,j0)) + |[1,1]|)) c= LeftComp f by A3, A5, A6, A55, A158, A159, Th4, NAT_1:13; A161: Int (cell ((GoB f),i1,j1)) is convex by A21, A27, Th17; Int (cell ((GoB f),i1,j1)) misses L~ f by A21, A27, GOBOARD7:12; then Int (cell ((GoB f),i1,j1)) c= (L~ f) ` by SUBSET_1:23; then A162: Int (cell ((GoB f),i1,j1)) c= LeftComp f by A55, A160, A30, A154, A156, A157, GOBOARD6:88, Th4, A161; A163: left_cell (f,(k + 1)) = cell ((GoB f),i1,j2) by A4, A5, A13, A14, A16, A17, A31, A45, A155, GOBOARD5:30; A164: LSeg ((((1 / 2) * (((GoB f) * (i1,j2)) + ((GoB f) * (i1,j1)))) + |[1,0]|),(((GoB f) * (i1,j1)) + |[1,1]|)) meets Int (cell ((GoB f),i1,j1)) by A30, A154, A156, A157, GOBOARD6:88; LSeg ((((1 / 2) * (((GoB f) * (i1,j2)) + ((GoB f) * (i1,j1)))) + |[1,0]|),(((GoB f) * (i1,j1)) + |[1,1]|)) misses L~ f by A30, A49, A154, A155, A156, A157, GOBOARD8:36; then LSeg ((((1 / 2) * (((GoB f) * (i1,j2)) + ((GoB f) * (i1,j1)))) + |[1,0]|),(((GoB f) * (i1,j1)) + |[1,1]|)) c= (L~ f) ` by SUBSET_1:23; then A165: LSeg ((((1 / 2) * (((GoB f) * (i1,j2)) + ((GoB f) * (i1,j1)))) + |[1,0]|),(((GoB f) * (i1,j1)) + |[1,1]|)) c= LeftComp f by A55, A162, A164, Th4; A166: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19; Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37; then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23; hence Int (left_cell (f,(k + 1))) c= LeftComp f by A55, A163, A165, A27, A28, A155, A156, GOBOARD6:86, Th4, A166; ::_thesis: verum end; supposethat A167: i0 + 1 = i1 and A168: j1 = j2 + 1 and A169: i1 <> len (GoB f) and A170: j0 = width (GoB f) ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f A171: left_cell (f,k) = cell ((GoB f),i0,j1) by A6, A7, A10, A11, A13, A14, A30, A46, A167, GOBOARD5:28; len (GoB f) > i1 by A21, A169, XXREAL_0:1; then A172: i1 + 1 <= len (GoB f) by NAT_1:13; A173: LSeg ((((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),j0)))) + |[0,1]|),(((1 / 2) * (((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i0 + 2),j0)))) + |[0,1]|)) meets Int (cell ((GoB f),i0,j1)) by A18, A21, A30, A167, A170, GOBOARD6:83; LSeg ((((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),j0)))) + |[0,1]|),(((1 / 2) * (((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i0 + 2),j0)))) + |[0,1]|)) misses L~ f by A18, A167, A170, A172, GOBOARD8:28; then LSeg ((((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),j0)))) + |[0,1]|),(((1 / 2) * (((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i0 + 2),j0)))) + |[0,1]|)) c= (L~ f) ` by SUBSET_1:23; then A174: LSeg ((((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),j0)))) + |[0,1]|),(((1 / 2) * (((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i0 + 2),j0)))) + |[0,1]|)) c= LeftComp f by A3, A5, A6, A55, A171, A173, Th4, NAT_1:13; A175: Int (cell ((GoB f),i1,j1)) is convex by A21, A27, Th17; Int (cell ((GoB f),i1,j1)) misses L~ f by A21, A27, GOBOARD7:12; then Int (cell ((GoB f),i1,j1)) c= (L~ f) ` by SUBSET_1:23; then A176: Int (cell ((GoB f),i1,j1)) c= LeftComp f by A55, A174, A20, A30, A167, A170, A172, GOBOARD6:83, Th4, A175; A177: left_cell (f,(k + 1)) = cell ((GoB f),i1,j2) by A4, A5, A13, A14, A16, A17, A31, A45, A168, GOBOARD5:30; A178: LSeg (((1 / 2) * (((GoB f) * ((i0 + 1),j2)) + ((GoB f) * ((i1 + 1),j0)))),(((1 / 2) * (((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i1 + 1),j0)))) + |[0,1]|)) meets Int (cell ((GoB f),i1,j1)) by A20, A30, A167, A170, A172, GOBOARD6:83; LSeg (((1 / 2) * (((GoB f) * ((i0 + 1),j2)) + ((GoB f) * ((i1 + 1),j0)))),(((1 / 2) * (((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i1 + 1),j0)))) + |[0,1]|)) misses L~ f by A5, A6, A11, A14, A17, A18, A30, A31, A49, A50, A51, A167, A168, A170, A172, GOBOARD8:10; then LSeg (((1 / 2) * (((GoB f) * ((i0 + 1),j2)) + ((GoB f) * ((i1 + 1),j0)))),(((1 / 2) * (((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i1 + 1),j0)))) + |[0,1]|)) c= (L~ f) ` by SUBSET_1:23; then A179: LSeg (((1 / 2) * (((GoB f) * ((i0 + 1),j2)) + ((GoB f) * ((i1 + 1),j0)))),(((1 / 2) * (((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i1 + 1),j0)))) + |[0,1]|)) c= LeftComp f by A55, A176, A178, Th4; A180: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19; Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37; then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23; hence Int (left_cell (f,(k + 1))) c= LeftComp f by A55, A177, A179, A20, A28, A30, A167, A168, A170, A172, GOBOARD6:82, Th4, A180; ::_thesis: verum end; supposethat A181: i0 + 1 = i1 and A182: j1 = j2 + 1 and A183: i1 = len (GoB f) and A184: j0 <> width (GoB f) ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f A185: left_cell (f,k) = cell ((GoB f),i0,j1) by A6, A7, A10, A11, A13, A14, A30, A46, A181, GOBOARD5:28; width (GoB f) > j0 by A25, A184, XXREAL_0:1; then A186: width (GoB f) >= j0 + 1 by NAT_1:13; A187: LSeg (((1 / 2) * (((GoB f) * (i0,j1)) + ((GoB f) * (i1,(j1 + 1))))),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i1,(j1 + 1))))) + |[1,0]|)) meets Int (cell ((GoB f),i0,j1)) by A18, A21, A26, A30, A181, A186, GOBOARD6:82; LSeg (((1 / 2) * (((GoB f) * (i0,j1)) + ((GoB f) * (i1,(j1 + 1))))),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i1,(j1 + 1))))) + |[1,0]|)) misses L~ f by A5, A6, A11, A14, A17, A28, A30, A31, A48, A50, A54, A181, A182, A183, A186, GOBOARD8:20; then LSeg (((1 / 2) * (((GoB f) * (i0,j1)) + ((GoB f) * (i1,(j1 + 1))))),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i1,(j1 + 1))))) + |[1,0]|)) c= (L~ f) ` by SUBSET_1:23; then A188: LSeg (((1 / 2) * (((GoB f) * (i0,j1)) + ((GoB f) * (i1,(j1 + 1))))),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i1,(j1 + 1))))) + |[1,0]|)) c= LeftComp f by A3, A5, A6, A55, A185, A187, Th4, NAT_1:13; A189: Int (cell ((GoB f),i1,j1)) is convex by A21, A27, Th17; Int (cell ((GoB f),i1,j1)) misses L~ f by A21, A27, GOBOARD7:12; then Int (cell ((GoB f),i1,j1)) c= (L~ f) ` by SUBSET_1:23; then A190: Int (cell ((GoB f),i1,j1)) c= LeftComp f by A55, A188, A26, A30, A181, A183, A186, GOBOARD6:86, Th4, A189; A191: left_cell (f,(k + 1)) = cell ((GoB f),i1,j2) by A4, A5, A13, A14, A16, A17, A31, A45, A182, GOBOARD5:30; A192: LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),j1)))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1))))) + |[1,0]|)) meets Int (cell ((GoB f),i1,j1)) by A26, A30, A181, A183, A186, GOBOARD6:86; LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),j1)))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1))))) + |[1,0]|)) misses L~ f by A28, A30, A54, A181, A182, A186, GOBOARD8:34; then LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),j1)))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1))))) + |[1,0]|)) c= (L~ f) ` by SUBSET_1:23; then A193: LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),j1)))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1))))) + |[1,0]|)) c= LeftComp f by A55, A190, A192, Th4; A194: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19; Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37; then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23; hence Int (left_cell (f,(k + 1))) c= LeftComp f by A55, A191, A193, A27, A28, A182, A183, GOBOARD6:86, Th4, A194; ::_thesis: verum end; supposethat A195: i0 + 1 = i1 and A196: j1 = j2 + 1 and A197: i1 <> len (GoB f) and A198: j0 <> width (GoB f) ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f A199: left_cell (f,k) = cell ((GoB f),i0,j1) by A6, A7, A10, A11, A13, A14, A30, A46, A195, GOBOARD5:28; len (GoB f) > i1 by A21, A197, XXREAL_0:1; then A200: i1 + 1 <= len (GoB f) by NAT_1:13; width (GoB f) > j0 by A25, A198, XXREAL_0:1; then A201: width (GoB f) >= j0 + 1 by NAT_1:13; A202: LSeg (((1 / 2) * (((GoB f) * (i0,(j2 + 1))) + ((GoB f) * ((i0 + 1),(j1 + 1))))),((1 / 2) * (((GoB f) * ((i0 + 1),(j2 + 1))) + ((GoB f) * ((i1 + 1),(j1 + 1)))))) meets Int (cell ((GoB f),i0,j1)) by A18, A21, A26, A30, A195, A196, A201, GOBOARD6:82; LSeg (((1 / 2) * (((GoB f) * (i0,(j2 + 1))) + ((GoB f) * ((i0 + 1),(j1 + 1))))),((1 / 2) * (((GoB f) * ((i0 + 1),(j2 + 1))) + ((GoB f) * ((i1 + 1),(j1 + 1)))))) misses L~ f by A5, A6, A11, A14, A17, A18, A28, A30, A31, A50, A51, A54, A195, A196, A200, A201, GOBOARD8:16; then LSeg (((1 / 2) * (((GoB f) * (i0,(j2 + 1))) + ((GoB f) * ((i0 + 1),(j1 + 1))))),((1 / 2) * (((GoB f) * ((i0 + 1),(j2 + 1))) + ((GoB f) * ((i1 + 1),(j1 + 1)))))) c= (L~ f) ` by SUBSET_1:23; then A203: LSeg (((1 / 2) * (((GoB f) * (i0,(j2 + 1))) + ((GoB f) * ((i0 + 1),(j1 + 1))))),((1 / 2) * (((GoB f) * ((i0 + 1),(j2 + 1))) + ((GoB f) * ((i1 + 1),(j1 + 1)))))) c= LeftComp f by A3, A5, A6, A55, A199, A202, Th4, NAT_1:13; A204: Int (cell ((GoB f),i1,j1)) is convex by A21, A27, Th17; Int (cell ((GoB f),i1,j1)) misses L~ f by A21, A27, GOBOARD7:12; then Int (cell ((GoB f),i1,j1)) c= (L~ f) ` by SUBSET_1:23; then A205: Int (cell ((GoB f),i1,j1)) c= LeftComp f by A55, A203, A20, A26, A30, A195, A196, A200, A201, GOBOARD6:82, Th4, A204; A206: left_cell (f,(k + 1)) = cell ((GoB f),i1,j2) by A4, A5, A13, A14, A16, A17, A31, A45, A196, GOBOARD5:30; A207: LSeg (((1 / 2) * (((GoB f) * ((i0 + 1),j2)) + ((GoB f) * ((i1 + 1),(j2 + 1))))),((1 / 2) * (((GoB f) * ((i0 + 1),(j2 + 1))) + ((GoB f) * ((i1 + 1),(j1 + 1)))))) meets Int (cell ((GoB f),i1,j1)) by A20, A26, A30, A195, A196, A200, A201, GOBOARD6:82; LSeg (((1 / 2) * (((GoB f) * ((i0 + 1),j2)) + ((GoB f) * ((i1 + 1),(j2 + 1))))),((1 / 2) * (((GoB f) * ((i0 + 1),(j2 + 1))) + ((GoB f) * ((i1 + 1),(j1 + 1)))))) misses L~ f by A5, A6, A11, A14, A17, A18, A28, A30, A31, A50, A51, A54, A195, A196, A200, A201, GOBOARD8:6; then LSeg (((1 / 2) * (((GoB f) * ((i0 + 1),j2)) + ((GoB f) * ((i1 + 1),(j2 + 1))))),((1 / 2) * (((GoB f) * ((i0 + 1),(j2 + 1))) + ((GoB f) * ((i1 + 1),(j1 + 1)))))) c= (L~ f) ` by SUBSET_1:23; then A208: LSeg (((1 / 2) * (((GoB f) * ((i0 + 1),j2)) + ((GoB f) * ((i1 + 1),(j2 + 1))))),((1 / 2) * (((GoB f) * ((i0 + 1),(j2 + 1))) + ((GoB f) * ((i1 + 1),(j1 + 1)))))) c= LeftComp f by A55, A205, A207, Th4; A209: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19; Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37; then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23; hence Int (left_cell (f,(k + 1))) c= LeftComp f by A55, A206, A208, A20, A27, A28, A195, A196, A200, GOBOARD6:82, Th4, A209; ::_thesis: verum end; supposethat A210: j0 + 1 = j1 and A211: i1 = i2 + 1 ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f left_cell (f,k) = cell ((GoB f),i2,j0) by A6, A7, A10, A11, A13, A14, A30, A210, A211, GOBOARD5:27 .= left_cell (f,(k + 1)) by A4, A5, A13, A14, A16, A17, A31, A210, A211, GOBOARD5:29 ; hence Int (left_cell (f,(k + 1))) c= LeftComp f by A3, A5, A6, NAT_1:13; ::_thesis: verum end; supposethat A212: i0 = i1 + 1 and A213: j1 + 1 = j2 and A214: i1 = 1 and A215: j1 = 1 ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f A216: left_cell (f,k) = cell ((GoB f),i1,(j1 -' 1)) by A6, A7, A10, A11, A13, A14, A30, A46, A212, GOBOARD5:29; i1 -' 1 <= i1 by NAT_D:35; then A217: i1 -' 1 <= len (GoB f) by A21, XXREAL_0:2; A218: j1 -' 1 = 0 by A215, XREAL_1:232; A219: i1 -' 1 = 0 by A214, XREAL_1:232; j1 -' 1 <= j1 by NAT_D:35; then A220: j1 -' 1 <= width (GoB f) by A27, XXREAL_0:2; A221: LSeg ((((GoB f) * (i1,j1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i0,j1)))) - |[0,1]|)) meets Int (cell ((GoB f),i1,(j1 -' 1))) by A19, A20, A212, A215, A218, GOBOARD6:84; LSeg ((((GoB f) * (i1,j1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i0,j1)))) - |[0,1]|)) misses L~ f by A212, A214, A215, GOBOARD8:26; then LSeg ((((GoB f) * (i1,j1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i0,j1)))) - |[0,1]|)) c= (L~ f) ` by SUBSET_1:23; then A222: LSeg ((((GoB f) * (i1,j1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i0,j1)))) - |[0,1]|)) c= LeftComp f by A3, A5, A6, A55, A216, A221, Th4, NAT_1:13; A223: Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) is convex by A217, A220, Th17; Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) misses L~ f by A217, A220, GOBOARD7:12; then Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) c= (L~ f) ` by SUBSET_1:23; then A224: Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) c= LeftComp f by A55, A222, A214, A215, A218, GOBOARD6:87, Th4, A223; A225: left_cell (f,(k + 1)) = cell ((GoB f),(i1 -' 1),j1) by A4, A5, A13, A14, A16, A17, A31, A45, A213, GOBOARD5:27; A226: LSeg ((((GoB f) * (i1,j1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i1,j2)))) - |[1,0]|)) meets Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) by A214, A215, A218, GOBOARD6:87; LSeg ((((GoB f) * (i1,j1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i1,j2)))) - |[1,0]|)) misses L~ f by A213, A214, A215, GOBOARD8:32; then LSeg ((((GoB f) * (i1,j1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i1,j2)))) - |[1,0]|)) c= (L~ f) ` by SUBSET_1:23; then A227: LSeg ((((GoB f) * (i1,j1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i1,j2)))) - |[1,0]|)) c= LeftComp f by A55, A224, A226, Th4; A228: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19; Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37; then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23; hence Int (left_cell (f,(k + 1))) c= LeftComp f by A55, A225, A227, A26, A29, A213, A214, A219, GOBOARD6:85, Th4, A228; ::_thesis: verum end; supposethat A229: i0 = i1 + 1 and A230: j1 + 1 = j2 and A231: i1 <> 1 and A232: j1 = 1 ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f A233: left_cell (f,k) = cell ((GoB f),i1,(j1 -' 1)) by A6, A7, A10, A11, A13, A14, A30, A46, A229, GOBOARD5:29; 1 < i1 by A20, A231, XXREAL_0:1; then A234: 1 <= i1 -' 1 by A45, NAT_1:13; A235: (i1 -' 1) + (1 + 1) = i0 by A45, A229; i1 -' 1 <= i1 by NAT_D:35; then A236: i1 -' 1 <= len (GoB f) by A21, XXREAL_0:2; A237: j1 -' 1 = 0 by A232, XREAL_1:232; j1 -' 1 <= j1 by NAT_D:35; then A238: j1 -' 1 <= width (GoB f) by A27, XXREAL_0:2; A239: LSeg ((((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * (i0,1)))) - |[0,1]|)) meets Int (cell ((GoB f),i1,(j1 -' 1))) by A19, A20, A229, A237, GOBOARD6:84; LSeg ((((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * (i0,1)))) - |[0,1]|)) misses L~ f by A19, A45, A234, A235, GOBOARD8:25; then LSeg ((((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * (i0,1)))) - |[0,1]|)) c= (L~ f) ` by SUBSET_1:23; then A240: LSeg ((((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * (i0,1)))) - |[0,1]|)) c= LeftComp f by A3, A5, A6, A55, A233, A239, Th4, NAT_1:13; A241: Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) is convex by A236, A238, Th17; Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) misses L~ f by A236, A238, GOBOARD7:12; then Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) c= (L~ f) ` by SUBSET_1:23; then A242: Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) c= LeftComp f by A55, A240, A21, A45, A234, A237, GOBOARD6:84, Th4, A241; A243: left_cell (f,(k + 1)) = cell ((GoB f),(i1 -' 1),j1) by A4, A5, A13, A14, A16, A17, A31, A45, A230, GOBOARD5:27; A244: LSeg ((((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,1)))) - |[0,1]|),((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,2))))) meets Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) by A21, A45, A234, A237, GOBOARD6:84; LSeg ((((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,1)))) - |[0,1]|),((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,2))))) misses L~ f by A5, A6, A11, A14, A17, A19, A30, A31, A45, A50, A230, A232, A234, A235, GOBOARD8:7; then LSeg ((((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,1)))) - |[0,1]|),((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,2))))) c= (L~ f) ` by SUBSET_1:23; then A245: LSeg ((((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,1)))) - |[0,1]|),((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,2))))) c= LeftComp f by A55, A242, A244, Th4; A246: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19; Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37; then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23; hence Int (left_cell (f,(k + 1))) c= LeftComp f by A55, A243, A245, A21, A29, A45, A230, A232, A234, GOBOARD6:82, Th4, A246; ::_thesis: verum end; supposethat A247: i0 = i1 + 1 and A248: j1 + 1 = j2 and A249: i1 = 1 and A250: j1 <> 1 ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f A251: left_cell (f,k) = cell ((GoB f),i1,(j1 -' 1)) by A6, A7, A10, A11, A13, A14, A30, A46, A247, GOBOARD5:29; 1 < j0 by A24, A30, A247, A250, XXREAL_0:1; then A252: 1 <= j0 -' 1 by A30, A46, A247, NAT_1:13; A253: (j0 -' 1) + (1 + 1) = j2 by A30, A46, A247, A248; A254: LSeg ((((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (1,((j1 -' 1) + 1))))) - |[1,0]|),((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (2,((j1 -' 1) + 1)))))) meets Int (cell ((GoB f),i1,(j1 -' 1))) by A19, A27, A30, A46, A247, A249, A252, GOBOARD6:82; LSeg ((((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (1,((j1 -' 1) + 1))))) - |[1,0]|),((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (2,((j1 -' 1) + 1)))))) misses L~ f by A5, A6, A11, A14, A17, A29, A30, A31, A46, A50, A247, A248, A249, A252, A253, GOBOARD8:17; then LSeg ((((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (1,((j1 -' 1) + 1))))) - |[1,0]|),((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (2,((j1 -' 1) + 1)))))) c= (L~ f) ` by SUBSET_1:23; then A255: LSeg ((((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (1,((j1 -' 1) + 1))))) - |[1,0]|),((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (2,((j1 -' 1) + 1)))))) c= LeftComp f by A3, A5, A6, A55, A251, A254, Th4, NAT_1:13; i1 -' 1 <= i1 by NAT_D:35; then A256: i1 -' 1 <= len (GoB f) by A21, XXREAL_0:2; A257: i1 -' 1 = 0 by A249, XREAL_1:232; j1 -' 1 <= j1 by NAT_D:35; then A258: j1 -' 1 <= width (GoB f) by A27, XXREAL_0:2; A259: Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) is convex by A256, A258, Th17; Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) misses L~ f by A256, A258, GOBOARD7:12; then Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) c= (L~ f) ` by SUBSET_1:23; then A260: Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) c= LeftComp f by A30, A55, A247, A255, A27, A46, A252, A257, GOBOARD6:85, Th4, A259; A261: left_cell (f,(k + 1)) = cell ((GoB f),(i1 -' 1),j1) by A4, A5, A13, A14, A16, A17, A31, A45, A248, GOBOARD5:27; A262: LSeg ((((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (1,((j1 -' 1) + 1))))) - |[1,0]|),(((1 / 2) * (((GoB f) * (1,((j1 -' 1) + 1))) + ((GoB f) * (1,((j1 -' 1) + 2))))) - |[1,0]|)) meets Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) by A27, A30, A46, A247, A252, A257, GOBOARD6:85; LSeg ((((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (1,((j1 -' 1) + 1))))) - |[1,0]|),(((1 / 2) * (((GoB f) * (1,((j1 -' 1) + 1))) + ((GoB f) * (1,((j1 -' 1) + 2))))) - |[1,0]|)) misses L~ f by A29, A30, A46, A247, A248, A252, GOBOARD8:31; then LSeg ((((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (1,((j1 -' 1) + 1))))) - |[1,0]|),(((1 / 2) * (((GoB f) * (1,((j1 -' 1) + 1))) + ((GoB f) * (1,((j1 -' 1) + 2))))) - |[1,0]|)) c= (L~ f) ` by SUBSET_1:23; then A263: LSeg ((((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (1,((j1 -' 1) + 1))))) - |[1,0]|),(((1 / 2) * (((GoB f) * (1,((j1 -' 1) + 1))) + ((GoB f) * (1,((j1 -' 1) + 2))))) - |[1,0]|)) c= LeftComp f by A55, A260, A262, Th4; A264: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19; Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37; then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23; hence Int (left_cell (f,(k + 1))) c= LeftComp f by A55, A261, A263, A26, A29, A46, A248, A257, GOBOARD6:85, Th4, A264; ::_thesis: verum end; supposethat A265: i0 = i1 + 1 and A266: j1 + 1 = j2 and A267: i1 <> 1 and A268: j1 <> 1 ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f A269: left_cell (f,k) = cell ((GoB f),i1,(j1 -' 1)) by A6, A7, A10, A11, A13, A14, A30, A46, A265, GOBOARD5:29; 1 < j0 by A24, A30, A265, A268, XXREAL_0:1; then A270: 1 <= j0 -' 1 by A30, A46, A265, NAT_1:13; 1 < i1 by A20, A267, XXREAL_0:1; then A271: 1 <= i1 -' 1 by A45, NAT_1:13; A272: (i1 -' 1) + (1 + 1) = i0 by A45, A265; A273: (j0 -' 1) + (1 + 1) = j2 by A30, A46, A265, A266; A274: LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),(j0 -' 1))) + ((GoB f) * (i1,j1)))),((1 / 2) * (((GoB f) * (i1,(j0 -' 1))) + ((GoB f) * (i0,j1))))) meets Int (cell ((GoB f),i1,(j1 -' 1))) by A19, A20, A27, A30, A46, A265, A270, GOBOARD6:82; LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),(j0 -' 1))) + ((GoB f) * (i1,j1)))),((1 / 2) * (((GoB f) * (i1,(j0 -' 1))) + ((GoB f) * (i0,j1))))) misses L~ f by A5, A6, A11, A14, A17, A19, A29, A30, A31, A45, A46, A50, A266, A270, A271, A272, A273, GOBOARD8:12; then LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),(j0 -' 1))) + ((GoB f) * (i1,j1)))),((1 / 2) * (((GoB f) * (i1,(j0 -' 1))) + ((GoB f) * (i0,j1))))) c= (L~ f) ` by SUBSET_1:23; then A275: LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),(j0 -' 1))) + ((GoB f) * (i1,j1)))),((1 / 2) * (((GoB f) * (i1,(j0 -' 1))) + ((GoB f) * (i0,j1))))) c= LeftComp f by A3, A5, A6, A55, A269, A274, Th4, NAT_1:13; i1 -' 1 <= i1 by NAT_D:35; then A276: i1 -' 1 <= len (GoB f) by A21, XXREAL_0:2; j1 -' 1 <= j1 by NAT_D:35; then A277: j1 -' 1 <= width (GoB f) by A27, XXREAL_0:2; A278: Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) is convex by A276, A277, Th17; Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) misses L~ f by A276, A277, GOBOARD7:12; then Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) c= (L~ f) ` by SUBSET_1:23; then A279: Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) c= LeftComp f by A30, A55, A265, A275, A21, A27, A45, A46, A270, A271, GOBOARD6:82, Th4, A278; A280: left_cell (f,(k + 1)) = cell ((GoB f),(i1 -' 1),j1) by A4, A5, A13, A14, A16, A17, A31, A45, A266, GOBOARD5:27; A281: LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),(j1 -' 1))) + ((GoB f) * (i1,j1)))),((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j2))))) meets Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) by A21, A27, A30, A45, A46, A265, A270, A271, GOBOARD6:82; LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),(j1 -' 1))) + ((GoB f) * (i1,j1)))),((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j2))))) misses L~ f by A5, A6, A11, A14, A17, A19, A29, A30, A31, A45, A46, A50, A266, A270, A271, A272, A273, GOBOARD8:2; then LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),(j1 -' 1))) + ((GoB f) * (i1,j1)))),((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j2))))) c= (L~ f) ` by SUBSET_1:23; then A282: LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),(j1 -' 1))) + ((GoB f) * (i1,j1)))),((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j2))))) c= LeftComp f by A55, A279, A281, Th4; A283: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19; Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37; then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23; hence Int (left_cell (f,(k + 1))) c= LeftComp f by A55, A280, A282, A21, A26, A29, A45, A266, A271, GOBOARD6:82, Th4, A283; ::_thesis: verum end; supposethat A284: j0 = j1 + 1 and A285: i1 + 1 = i2 ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f left_cell (f,k) = cell ((GoB f),i0,j1) by A6, A7, A10, A11, A13, A14, A30, A45, A284, GOBOARD5:30 .= left_cell (f,(k + 1)) by A4, A5, A13, A14, A16, A17, A30, A31, A46, A284, A285, GOBOARD5:28 ; hence Int (left_cell (f,(k + 1))) c= LeftComp f by A3, A5, A6, NAT_1:13; ::_thesis: verum end; supposethat A286: i0 + 1 = i1 and A287: i1 + 1 = i2 and A288: j0 = width (GoB f) ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f A289: left_cell (f,k) = cell ((GoB f),i0,(width (GoB f))) by A6, A7, A10, A11, A13, A14, A30, A49, A286, A288, GOBOARD5:28; A290: left_cell (f,(k + 1)) = cell ((GoB f),i1,(width (GoB f))) by A4, A5, A13, A14, A16, A17, A30, A31, A49, A286, A287, A288, GOBOARD5:28; A291: LSeg ((((1 / 2) * (((GoB f) * (i0,(width (GoB f)))) + ((GoB f) * ((i0 + 1),(width (GoB f)))))) + |[0,1]|),(((1 / 2) * (((GoB f) * (i1,(width (GoB f)))) + ((GoB f) * ((i1 + 1),(width (GoB f)))))) + |[0,1]|)) meets Int (cell ((GoB f),i0,(width (GoB f)))) by A18, A21, A286, GOBOARD6:83; LSeg ((((1 / 2) * (((GoB f) * (i0,(width (GoB f)))) + ((GoB f) * ((i0 + 1),(width (GoB f)))))) + |[0,1]|),(((1 / 2) * (((GoB f) * (i1,(width (GoB f)))) + ((GoB f) * ((i1 + 1),(width (GoB f)))))) + |[0,1]|)) misses L~ f by A18, A23, A51, A286, A287, GOBOARD8:28; then LSeg ((((1 / 2) * (((GoB f) * (i0,(width (GoB f)))) + ((GoB f) * ((i0 + 1),(width (GoB f)))))) + |[0,1]|),(((1 / 2) * (((GoB f) * (i1,(width (GoB f)))) + ((GoB f) * ((i1 + 1),(width (GoB f)))))) + |[0,1]|)) c= (L~ f) ` by SUBSET_1:23; then A292: LSeg ((((1 / 2) * (((GoB f) * (i0,(width (GoB f)))) + ((GoB f) * ((i0 + 1),(width (GoB f)))))) + |[0,1]|),(((1 / 2) * (((GoB f) * (i1,(width (GoB f)))) + ((GoB f) * ((i1 + 1),(width (GoB f)))))) + |[0,1]|)) c= LeftComp f by A3, A5, A6, A55, A289, A291, Th4, NAT_1:13; A293: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19; Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37; then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23; hence Int (left_cell (f,(k + 1))) c= LeftComp f by A55, A290, A292, A20, A23, A287, GOBOARD6:83, Th4, A293; ::_thesis: verum end; supposethat A294: i0 + 1 = i1 and A295: i1 + 1 = i2 and A296: j0 <> width (GoB f) ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f A297: left_cell (f,k) = cell ((GoB f),i0,j1) by A6, A7, A10, A11, A13, A14, A30, A46, A294, GOBOARD5:28; width (GoB f) > j0 by A25, A296, XXREAL_0:1; then A298: width (GoB f) >= j0 + 1 by NAT_1:13; A299: left_cell (f,(k + 1)) = cell ((GoB f),i1,j1) by A4, A5, A13, A14, A16, A17, A31, A46, A295, GOBOARD5:28; A300: LSeg (((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),(j0 + 1))))),((1 / 2) * (((GoB f) * (i1,j0)) + ((GoB f) * ((i1 + 1),(j0 + 1)))))) meets Int (cell ((GoB f),i0,j1)) by A18, A21, A26, A30, A294, A298, GOBOARD6:82; LSeg (((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),(j0 + 1))))),((1 / 2) * (((GoB f) * (i1,j0)) + ((GoB f) * ((i1 + 1),(j0 + 1)))))) misses L~ f by A5, A6, A11, A14, A17, A18, A23, A24, A30, A31, A50, A51, A294, A295, A298, GOBOARD8:14; then LSeg (((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),(j0 + 1))))),((1 / 2) * (((GoB f) * (i1,j0)) + ((GoB f) * ((i1 + 1),(j0 + 1)))))) c= (L~ f) ` by SUBSET_1:23; then A301: LSeg (((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),(j0 + 1))))),((1 / 2) * (((GoB f) * (i1,j0)) + ((GoB f) * ((i1 + 1),(j0 + 1)))))) c= LeftComp f by A3, A5, A6, A55, A297, A300, Th4, NAT_1:13; A302: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19; Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37; then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23; hence Int (left_cell (f,(k + 1))) c= LeftComp f by A55, A299, A301, A20, A23, A24, A30, A294, A295, A298, GOBOARD6:82, Th4, A302; ::_thesis: verum end; supposethat A303: i0 + 1 = i1 and A304: j1 + 1 = j2 ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f left_cell (f,k) = cell ((GoB f),i0,j1) by A6, A7, A10, A11, A13, A14, A30, A46, A303, GOBOARD5:28 .= left_cell (f,(k + 1)) by A4, A5, A13, A14, A16, A17, A31, A303, A304, GOBOARD5:27 ; hence Int (left_cell (f,(k + 1))) c= LeftComp f by A3, A5, A6, NAT_1:13; ::_thesis: verum end; supposethat A305: j0 + 1 = j1 and A306: i1 + 1 = i2 and A307: i0 = 1 and A308: j1 = width (GoB f) ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f A309: left_cell (f,k) = cell ((GoB f),(i1 -' 1),j0) by A6, A7, A10, A11, A13, A14, A30, A45, A305, GOBOARD5:27; A310: i0 -' 1 = 0 by A307, XREAL_1:232; A311: j1 -' 1 = j0 by A305, NAT_D:34; A312: LSeg ((((1 / 2) * (((GoB f) * (1,j0)) + ((GoB f) * (1,j1)))) - |[1,0]|),(((GoB f) * (1,j1)) + |[(- 1),1]|)) meets Int (cell ((GoB f),(i1 -' 1),j0)) by A24, A27, A30, A305, A310, GOBOARD6:85; LSeg ((((1 / 2) * (((GoB f) * (1,j0)) + ((GoB f) * (1,j1)))) - |[1,0]|),(((GoB f) * (1,j1)) + |[(- 1),1]|)) misses L~ f by A308, A311, GOBOARD8:33; then LSeg ((((1 / 2) * (((GoB f) * (1,j0)) + ((GoB f) * (1,j1)))) - |[1,0]|),(((GoB f) * (1,j1)) + |[(- 1),1]|)) c= (L~ f) ` by SUBSET_1:23; then A313: LSeg ((((1 / 2) * (((GoB f) * (1,j0)) + ((GoB f) * (1,j1)))) - |[1,0]|),(((GoB f) * (1,j1)) + |[(- 1),1]|)) c= LeftComp f by A3, A5, A6, A55, A309, A312, Th4, NAT_1:13; i1 -' 1 <= i1 by NAT_D:35; then A314: i1 -' 1 <= len (GoB f) by A21, XXREAL_0:2; A315: Int (cell ((GoB f),(i1 -' 1),j1)) is convex by A27, A314, Th17; Int (cell ((GoB f),(i1 -' 1),j1)) misses L~ f by A27, A314, GOBOARD7:12; then Int (cell ((GoB f),(i1 -' 1),j1)) c= (L~ f) ` by SUBSET_1:23; then A316: Int (cell ((GoB f),(i1 -' 1),j1)) c= LeftComp f by A30, A55, A305, A313, A308, A310, GOBOARD6:89, Th4, A315; A317: left_cell (f,(k + 1)) = cell ((GoB f),i1,j1) by A4, A5, A13, A14, A16, A17, A31, A305, A306, GOBOARD5:28; A318: LSeg ((((GoB f) * (1,j1)) + |[(- 1),1]|),(((1 / 2) * (((GoB f) * (1,j1)) + ((GoB f) * (2,j1)))) + |[0,1]|)) meets Int (cell ((GoB f),(i1 -' 1),j1)) by A30, A305, A308, A310, GOBOARD6:89; LSeg ((((GoB f) * (1,j1)) + |[(- 1),1]|),(((1 / 2) * (((GoB f) * (1,j1)) + ((GoB f) * (2,j1)))) + |[0,1]|)) misses L~ f by A308, GOBOARD8:29; then LSeg ((((GoB f) * (1,j1)) + |[(- 1),1]|),(((1 / 2) * (((GoB f) * (1,j1)) + ((GoB f) * (2,j1)))) + |[0,1]|)) c= (L~ f) ` by SUBSET_1:23; then A319: LSeg ((((GoB f) * (1,j1)) + |[(- 1),1]|),(((1 / 2) * (((GoB f) * (1,j1)) + ((GoB f) * (2,j1)))) + |[0,1]|)) c= LeftComp f by A55, A316, A318, Th4; A320: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19; Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37; then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23; hence Int (left_cell (f,(k + 1))) c= LeftComp f by A55, A317, A319, A23, A30, A305, A306, A307, A308, GOBOARD6:83, Th4, A320; ::_thesis: verum end; supposethat A321: j0 + 1 = j1 and A322: i1 + 1 = i2 and A323: i0 <> 1 and A324: j1 = width (GoB f) ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f A325: left_cell (f,k) = cell ((GoB f),(i1 -' 1),j0) by A6, A7, A10, A11, A13, A14, A30, A45, A321, GOBOARD5:27; 1 < i0 by A18, A323, XXREAL_0:1; then A326: 1 <= i0 -' 1 by A30, A45, A321, NAT_1:13; A327: j1 -' 1 = j0 by A321, NAT_D:34; A328: (i1 -' 1) + (1 + 1) = i2 by A45, A322; A329: LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),j0)) + ((GoB f) * (i1,j1)))),(((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j1)))) + |[0,1]|)) meets Int (cell ((GoB f),(i1 -' 1),j0)) by A21, A24, A27, A30, A45, A321, A326, GOBOARD6:82; LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),j0)) + ((GoB f) * (i1,j1)))),(((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j1)))) + |[0,1]|)) misses L~ f by A5, A6, A11, A14, A17, A23, A30, A31, A45, A50, A321, A324, A326, A327, A328, GOBOARD8:9; then LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),j0)) + ((GoB f) * (i1,j1)))),(((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j1)))) + |[0,1]|)) c= (L~ f) ` by SUBSET_1:23; then A330: LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),j0)) + ((GoB f) * (i1,j1)))),(((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j1)))) + |[0,1]|)) c= LeftComp f by A3, A5, A6, A55, A325, A329, Th4, NAT_1:13; i1 -' 1 <= i1 by NAT_D:35; then A331: i1 -' 1 <= len (GoB f) by A21, XXREAL_0:2; A332: Int (cell ((GoB f),(i1 -' 1),j1)) is convex by A27, A331, Th17; Int (cell ((GoB f),(i1 -' 1),j1)) misses L~ f by A27, A331, GOBOARD7:12; then Int (cell ((GoB f),(i1 -' 1),j1)) c= (L~ f) ` by SUBSET_1:23; then A333: Int (cell ((GoB f),(i1 -' 1),j1)) c= LeftComp f by A30, A55, A321, A330, A19, A45, A324, A326, GOBOARD6:83, Th4, A332; A334: left_cell (f,(k + 1)) = cell ((GoB f),i1,j1) by A4, A5, A13, A14, A16, A17, A31, A321, A322, GOBOARD5:28; A335: LSeg ((((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j1)))) + |[0,1]|),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i2,j1)))) + |[0,1]|)) meets Int (cell ((GoB f),(i1 -' 1),j1)) by A21, A30, A45, A321, A324, A326, GOBOARD6:83; LSeg ((((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j1)))) + |[0,1]|),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i2,j1)))) + |[0,1]|)) misses L~ f by A23, A30, A45, A321, A324, A326, A328, GOBOARD8:28; then LSeg ((((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j1)))) + |[0,1]|),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i2,j1)))) + |[0,1]|)) c= (L~ f) ` by SUBSET_1:23; then A336: LSeg ((((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j1)))) + |[0,1]|),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i2,j1)))) + |[0,1]|)) c= LeftComp f by A55, A333, A335, Th4; A337: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19; Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37; then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23; hence Int (left_cell (f,(k + 1))) c= LeftComp f by A55, A334, A336, A20, A23, A322, A324, GOBOARD6:83, Th4, A337; ::_thesis: verum end; supposethat A338: j0 + 1 = j1 and A339: i1 + 1 = i2 and A340: i0 = 1 and A341: j1 <> width (GoB f) ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f A342: left_cell (f,k) = cell ((GoB f),(i1 -' 1),j0) by A6, A7, A10, A11, A13, A14, A30, A45, A338, GOBOARD5:27; width (GoB f) > j1 by A27, A341, XXREAL_0:1; then A343: width (GoB f) >= j1 + 1 by NAT_1:13; A344: i0 -' 1 = 0 by A340, XREAL_1:232; A345: LSeg ((((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * (i0,j1)))) - |[1,0]|),(((1 / 2) * (((GoB f) * (i0,j1)) + ((GoB f) * (i0,(j1 + 1))))) - |[1,0]|)) meets Int (cell ((GoB f),(i1 -' 1),j0)) by A24, A27, A30, A338, A340, A344, GOBOARD6:85; LSeg ((((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * (i0,j1)))) - |[1,0]|),(((1 / 2) * (((GoB f) * (i0,j1)) + ((GoB f) * (i0,(j1 + 1))))) - |[1,0]|)) misses L~ f by A24, A53, A338, A340, A343, GOBOARD8:31; then LSeg ((((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * (i0,j1)))) - |[1,0]|),(((1 / 2) * (((GoB f) * (i0,j1)) + ((GoB f) * (i0,(j1 + 1))))) - |[1,0]|)) c= (L~ f) ` by SUBSET_1:23; then A346: LSeg ((((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * (i0,j1)))) - |[1,0]|),(((1 / 2) * (((GoB f) * (i0,j1)) + ((GoB f) * (i0,(j1 + 1))))) - |[1,0]|)) c= LeftComp f by A3, A5, A6, A55, A342, A345, Th4, NAT_1:13; i1 -' 1 <= i1 by NAT_D:35; then A347: i1 -' 1 <= len (GoB f) by A21, XXREAL_0:2; A348: Int (cell ((GoB f),(i1 -' 1),j1)) is convex by A27, A347, Th17; Int (cell ((GoB f),(i1 -' 1),j1)) misses L~ f by A27, A347, GOBOARD7:12; then Int (cell ((GoB f),(i1 -' 1),j1)) c= (L~ f) ` by SUBSET_1:23; then A349: Int (cell ((GoB f),(i1 -' 1),j1)) c= LeftComp f by A30, A55, A338, A346, A26, A340, A343, A344, GOBOARD6:85, Th4, A348; A350: left_cell (f,(k + 1)) = cell ((GoB f),i1,j1) by A4, A5, A13, A14, A16, A17, A31, A338, A339, GOBOARD5:28; A351: LSeg ((((1 / 2) * (((GoB f) * (i1,(j0 + 1))) + ((GoB f) * (i1,(j0 + 2))))) - |[1,0]|),((1 / 2) * (((GoB f) * (i1,(j0 + 1))) + ((GoB f) * (i2,(j0 + 2)))))) meets Int (cell ((GoB f),(i1 -' 1),j1)) by A26, A30, A338, A340, A343, A344, GOBOARD6:85; LSeg ((((1 / 2) * (((GoB f) * (i1,(j0 + 1))) + ((GoB f) * (i1,(j0 + 2))))) - |[1,0]|),((1 / 2) * (((GoB f) * (i1,(j0 + 1))) + ((GoB f) * (i2,(j0 + 2)))))) misses L~ f by A5, A6, A11, A14, A17, A24, A30, A31, A50, A338, A339, A340, A343, GOBOARD8:18; then LSeg ((((1 / 2) * (((GoB f) * (i1,(j0 + 1))) + ((GoB f) * (i1,(j0 + 2))))) - |[1,0]|),((1 / 2) * (((GoB f) * (i1,(j0 + 1))) + ((GoB f) * (i2,(j0 + 2)))))) c= (L~ f) ` by SUBSET_1:23; then A352: LSeg ((((1 / 2) * (((GoB f) * (i1,(j0 + 1))) + ((GoB f) * (i1,(j0 + 2))))) - |[1,0]|),((1 / 2) * (((GoB f) * (i1,(j0 + 1))) + ((GoB f) * (i2,(j0 + 2)))))) c= LeftComp f by A55, A349, A351, Th4; A353: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19; Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37; then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23; hence Int (left_cell (f,(k + 1))) c= LeftComp f by A55, A350, A352, A20, A23, A26, A338, A339, A343, GOBOARD6:82, Th4, A353; ::_thesis: verum end; supposethat A354: j0 + 1 = j1 and A355: i1 + 1 = i2 and A356: i0 <> 1 and A357: j1 <> width (GoB f) ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f A358: left_cell (f,k) = cell ((GoB f),(i1 -' 1),j0) by A6, A7, A10, A11, A13, A14, A30, A45, A354, GOBOARD5:27; 1 < i0 by A18, A356, XXREAL_0:1; then A359: 1 <= i0 -' 1 by A30, A45, A354, NAT_1:13; width (GoB f) > j1 by A27, A357, XXREAL_0:1; then A360: width (GoB f) >= j1 + 1 by NAT_1:13; A361: (i1 -' 1) + (1 + 1) = i2 by A45, A355; A362: LSeg (((1 / 2) * (((GoB f) * ((i0 -' 1),j0)) + ((GoB f) * (i0,j1)))),((1 / 2) * (((GoB f) * ((i0 -' 1),j1)) + ((GoB f) * (i0,(j1 + 1)))))) meets Int (cell ((GoB f),(i1 -' 1),j0)) by A21, A24, A27, A30, A45, A354, A359, GOBOARD6:82; LSeg (((1 / 2) * (((GoB f) * ((i0 -' 1),j0)) + ((GoB f) * (i0,j1)))),((1 / 2) * (((GoB f) * ((i0 -' 1),j1)) + ((GoB f) * (i0,(j1 + 1)))))) misses L~ f by A5, A6, A11, A14, A17, A23, A24, A30, A31, A45, A50, A53, A354, A359, A360, A361, GOBOARD8:3; then LSeg (((1 / 2) * (((GoB f) * ((i0 -' 1),j0)) + ((GoB f) * (i0,j1)))),((1 / 2) * (((GoB f) * ((i0 -' 1),j1)) + ((GoB f) * (i0,(j1 + 1)))))) c= (L~ f) ` by SUBSET_1:23; then A363: LSeg (((1 / 2) * (((GoB f) * ((i0 -' 1),j0)) + ((GoB f) * (i0,j1)))),((1 / 2) * (((GoB f) * ((i0 -' 1),j1)) + ((GoB f) * (i0,(j1 + 1)))))) c= LeftComp f by A3, A5, A6, A55, A358, A362, Th4, NAT_1:13; i1 -' 1 <= i1 by NAT_D:35; then A364: i1 -' 1 <= len (GoB f) by A21, XXREAL_0:2; A365: Int (cell ((GoB f),(i1 -' 1),j1)) is convex by A27, A364, Th17; Int (cell ((GoB f),(i1 -' 1),j1)) misses L~ f by A27, A364, GOBOARD7:12; then Int (cell ((GoB f),(i1 -' 1),j1)) c= (L~ f) ` by SUBSET_1:23; then A366: Int (cell ((GoB f),(i1 -' 1),j1)) c= LeftComp f by A30, A55, A354, A363, A19, A26, A45, A359, A360, GOBOARD6:82, Th4, A365; A367: left_cell (f,(k + 1)) = cell ((GoB f),i1,j1) by A4, A5, A13, A14, A16, A17, A31, A354, A355, GOBOARD5:28; A368: LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,(j1 + 1))))),((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i2,(j1 + 1)))))) meets Int (cell ((GoB f),(i1 -' 1),j1)) by A21, A26, A30, A45, A354, A359, A360, GOBOARD6:82; LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,(j1 + 1))))),((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i2,(j1 + 1)))))) misses L~ f by A5, A6, A11, A14, A17, A23, A24, A30, A31, A45, A50, A53, A354, A359, A360, A361, GOBOARD8:15; then LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,(j1 + 1))))),((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i2,(j1 + 1)))))) c= (L~ f) ` by SUBSET_1:23; then A369: LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,(j1 + 1))))),((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i2,(j1 + 1)))))) c= LeftComp f by A55, A366, A368, Th4; A370: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19; Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37; then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23; hence Int (left_cell (f,(k + 1))) c= LeftComp f by A55, A367, A369, A20, A23, A26, A355, A360, GOBOARD6:82, Th4, A370; ::_thesis: verum end; supposethat A371: j0 + 1 = j1 and A372: j1 + 1 = j2 and A373: i0 = 1 ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f A374: left_cell (f,k) = cell ((GoB f),0,j0) by A6, A7, A10, A11, A13, A14, A30, A56, A371, A373, GOBOARD5:27; A375: left_cell (f,(k + 1)) = cell ((GoB f),0,j1) by A4, A5, A13, A14, A16, A17, A30, A31, A56, A371, A372, A373, GOBOARD5:27; A376: LSeg ((((1 / 2) * (((GoB f) * (1,j0)) + ((GoB f) * (1,j1)))) - |[1,0]|),(((1 / 2) * (((GoB f) * (1,j1)) + ((GoB f) * (1,j2)))) - |[1,0]|)) meets Int (cell ((GoB f),0,j0)) by A24, A27, A371, GOBOARD6:85; LSeg ((((1 / 2) * (((GoB f) * (1,j0)) + ((GoB f) * (1,j1)))) - |[1,0]|),(((1 / 2) * (((GoB f) * (1,j1)) + ((GoB f) * (1,j2)))) - |[1,0]|)) misses L~ f by A24, A29, A53, A371, A372, GOBOARD8:31; then LSeg ((((1 / 2) * (((GoB f) * (1,j0)) + ((GoB f) * (1,j1)))) - |[1,0]|),(((1 / 2) * (((GoB f) * (1,j1)) + ((GoB f) * (1,j2)))) - |[1,0]|)) c= (L~ f) ` by SUBSET_1:23; then A377: LSeg ((((1 / 2) * (((GoB f) * (1,j0)) + ((GoB f) * (1,j1)))) - |[1,0]|),(((1 / 2) * (((GoB f) * (1,j1)) + ((GoB f) * (1,j2)))) - |[1,0]|)) c= LeftComp f by A3, A5, A6, A55, A374, A376, Th4, NAT_1:13; A378: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19; Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37; then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23; hence Int (left_cell (f,(k + 1))) c= LeftComp f by A55, A375, A377, A26, A29, A372, GOBOARD6:85, Th4, A378; ::_thesis: verum end; supposethat A379: j0 + 1 = j1 and A380: j1 + 1 = j2 and A381: i0 <> 1 ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f A382: left_cell (f,k) = cell ((GoB f),(i1 -' 1),j0) by A6, A7, A10, A11, A13, A14, A30, A45, A379, GOBOARD5:27; 1 < i0 by A18, A381, XXREAL_0:1; then A383: 1 <= i0 -' 1 by A30, A45, A379, NAT_1:13; A384: left_cell (f,(k + 1)) = cell ((GoB f),(i1 -' 1),j1) by A4, A5, A13, A14, A16, A17, A31, A45, A380, GOBOARD5:27; A385: LSeg (((1 / 2) * (((GoB f) * ((i0 -' 1),j0)) + ((GoB f) * (i0,j1)))),((1 / 2) * (((GoB f) * ((i0 -' 1),j1)) + ((GoB f) * (i0,j2))))) meets Int (cell ((GoB f),(i1 -' 1),j0)) by A21, A24, A27, A30, A45, A379, A383, GOBOARD6:82; LSeg (((1 / 2) * (((GoB f) * ((i0 -' 1),j0)) + ((GoB f) * (i0,j1)))),((1 / 2) * (((GoB f) * ((i0 -' 1),j1)) + ((GoB f) * (i0,j2))))) misses L~ f by A5, A6, A11, A14, A17, A19, A24, A29, A30, A31, A45, A50, A53, A379, A380, A383, GOBOARD8:1; then LSeg (((1 / 2) * (((GoB f) * ((i0 -' 1),j0)) + ((GoB f) * (i0,j1)))),((1 / 2) * (((GoB f) * ((i0 -' 1),j1)) + ((GoB f) * (i0,j2))))) c= (L~ f) ` by SUBSET_1:23; then A386: LSeg (((1 / 2) * (((GoB f) * ((i0 -' 1),j0)) + ((GoB f) * (i0,j1)))),((1 / 2) * (((GoB f) * ((i0 -' 1),j1)) + ((GoB f) * (i0,j2))))) c= LeftComp f by A3, A5, A6, A55, A382, A385, Th4, NAT_1:13; A387: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19; Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37; then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23; hence Int (left_cell (f,(k + 1))) c= LeftComp f by A30, A55, A379, A384, A386, A19, A26, A29, A45, A380, A383, GOBOARD6:82, Th4, A387; ::_thesis: verum end; end; end; hence Int (left_cell (f,(k + 1))) c= LeftComp f ; ::_thesis: verum end; end; end; end; thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A1, A2); ::_thesis: verum end; theorem :: GOBOARD9:22 for f being non constant standard special_circular_sequence holds GoB (Rev f) = GoB f by Lm1; theorem Th23: :: GOBOARD9:23 for f being non constant standard special_circular_sequence holds RightComp f = LeftComp (Rev f) proof let f be non constant standard special_circular_sequence; ::_thesis: RightComp f = LeftComp (Rev f) LeftComp (Rev f) is_a_component_of (L~ (Rev f)) ` by Def1; then A1: LeftComp (Rev f) is_a_component_of (L~ f) ` by SPPOL_2:22; A2: len f >= 4 by GOBOARD7:34; A3: len f >= 1 + 1 by GOBOARD7:34, XXREAL_0:2; A4: ((len f) -' 1) + 1 = len f by A2, XREAL_1:235, XXREAL_0:2; then A5: 1 <= (len f) -' 1 by A3, XREAL_1:6; A6: ((len f) -' 1) + 1 <= len (Rev f) by A4, FINSEQ_5:def_3; right_cell (f,1) = left_cell ((Rev f),((len f) -' 1)) by A4, A5, Th10; then Int (right_cell (f,1)) c= LeftComp (Rev f) by A5, A6, Th21; hence RightComp f = LeftComp (Rev f) by A1, Def2; ::_thesis: verum end; theorem :: GOBOARD9:24 for f being non constant standard special_circular_sequence holds RightComp (Rev f) = LeftComp f proof let f be non constant standard special_circular_sequence; ::_thesis: RightComp (Rev f) = LeftComp f Rev (Rev f) = f ; hence RightComp (Rev f) = LeftComp f by Th23; ::_thesis: verum end; theorem :: GOBOARD9:25 for f being non constant standard special_circular_sequence for k being Element of NAT st 1 <= k & k + 1 <= len f holds Int (right_cell (f,k)) c= RightComp f proof let f be non constant standard special_circular_sequence; ::_thesis: for k being Element of NAT st 1 <= k & k + 1 <= len f holds Int (right_cell (f,k)) c= RightComp f let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f implies Int (right_cell (f,k)) c= RightComp f ) assume that A1: 1 <= k and A2: k + 1 <= len f ; ::_thesis: Int (right_cell (f,k)) c= RightComp f A3: len f = len (Rev f) by FINSEQ_5:def_3; k <= len f by A2, NAT_1:13; then A4: ((len f) -' k) + k = len f by XREAL_1:235; then A5: 1 <= (len f) -' k by A2, XREAL_1:6; A6: ((len f) -' k) + 1 <= len f by A1, A4, XREAL_1:6; A7: right_cell (f,k) = left_cell ((Rev f),((len f) -' k)) by A1, A4, A5, Th10; RightComp f = LeftComp (Rev f) by Th23; hence Int (right_cell (f,k)) c= RightComp f by A3, A5, A6, A7, Th21; ::_thesis: verum end;