:: GOBRD12 semantic presentation begin Lm1: for f being non constant standard special_circular_sequence holds (L~ f) ` = the carrier of ((TOP-REAL 2) | ((L~ f) `)) proof let f be non constant standard special_circular_sequence; ::_thesis: (L~ f) ` = the carrier of ((TOP-REAL 2) | ((L~ f) `)) (L~ f) ` = [#] ((TOP-REAL 2) | ((L~ f) `)) by PRE_TOPC:def_5 .= the carrier of ((TOP-REAL 2) | ((L~ f) `)) ; hence (L~ f) ` = the carrier of ((TOP-REAL 2) | ((L~ f) `)) ; ::_thesis: verum end; Lm2: the carrier of (TOP-REAL 2) = REAL 2 by EUCLID:22; theorem Th1: :: GOBRD12:1 for f being non constant standard special_circular_sequence for i, j being Element of NAT st i <= len (GoB f) & j <= width (GoB f) holds Int (cell ((GoB f),i,j)) c= (L~ f) ` proof let f be non constant standard special_circular_sequence; ::_thesis: for i, j being Element of NAT st i <= len (GoB f) & j <= width (GoB f) holds Int (cell ((GoB f),i,j)) c= (L~ f) ` let i, j be Element of NAT ; ::_thesis: ( i <= len (GoB f) & j <= width (GoB f) implies Int (cell ((GoB f),i,j)) c= (L~ f) ` ) assume ( i <= len (GoB f) & j <= width (GoB f) ) ; ::_thesis: Int (cell ((GoB f),i,j)) c= (L~ f) ` then Int (cell ((GoB f),i,j)) misses L~ f by GOBOARD7:12; hence Int (cell ((GoB f),i,j)) c= (L~ f) ` by SUBSET_1:23; ::_thesis: verum end; theorem Th2: :: GOBRD12:2 for f being non constant standard special_circular_sequence for i, j being Element of NAT st i <= len (GoB f) & j <= width (GoB f) holds Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `))) = (cell ((GoB f),i,j)) /\ ((L~ f) `) proof let f be non constant standard special_circular_sequence; ::_thesis: for i, j being Element of NAT st i <= len (GoB f) & j <= width (GoB f) holds Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `))) = (cell ((GoB f),i,j)) /\ ((L~ f) `) let i, j be Element of NAT ; ::_thesis: ( i <= len (GoB f) & j <= width (GoB f) implies Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `))) = (cell ((GoB f),i,j)) /\ ((L~ f) `) ) reconsider V = Int (cell ((GoB f),i,j)) as Subset of (TOP-REAL 2) ; reconsider B = (L~ f) ` as Subset of (TOP-REAL 2) ; assume A1: ( i <= len (GoB f) & j <= width (GoB f) ) ; ::_thesis: Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `))) = (cell ((GoB f),i,j)) /\ ((L~ f) `) then Cl (Down (V,B)) = (Cl V) /\ B by Th1, CONNSP_3:29; hence Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `))) = (cell ((GoB f),i,j)) /\ ((L~ f) `) by A1, GOBRD11:35; ::_thesis: verum end; theorem Th3: :: GOBRD12:3 for f being non constant standard special_circular_sequence for i, j being Element of NAT st i <= len (GoB f) & j <= width (GoB f) holds ( Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `))) is connected & Down ((Int (cell ((GoB f),i,j))),((L~ f) `)) = Int (cell ((GoB f),i,j)) ) proof let f be non constant standard special_circular_sequence; ::_thesis: for i, j being Element of NAT st i <= len (GoB f) & j <= width (GoB f) holds ( Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `))) is connected & Down ((Int (cell ((GoB f),i,j))),((L~ f) `)) = Int (cell ((GoB f),i,j)) ) let i, j be Element of NAT ; ::_thesis: ( i <= len (GoB f) & j <= width (GoB f) implies ( Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `))) is connected & Down ((Int (cell ((GoB f),i,j))),((L~ f) `)) = Int (cell ((GoB f),i,j)) ) ) assume A1: ( i <= len (GoB f) & j <= width (GoB f) ) ; ::_thesis: ( Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `))) is connected & Down ((Int (cell ((GoB f),i,j))),((L~ f) `)) = Int (cell ((GoB f),i,j)) ) then ( Int (cell ((GoB f),i,j)) is convex & Down ((Int (cell ((GoB f),i,j))),((L~ f) `)) = Int (cell ((GoB f),i,j)) ) by Th1, GOBOARD9:17, XBOOLE_1:28; then Down ((Int (cell ((GoB f),i,j))),((L~ f) `)) is connected by CONNSP_1:23; hence Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `))) is connected by CONNSP_1:19; ::_thesis: Down ((Int (cell ((GoB f),i,j))),((L~ f) `)) = Int (cell ((GoB f),i,j)) thus Down ((Int (cell ((GoB f),i,j))),((L~ f) `)) = Int (cell ((GoB f),i,j)) by A1, Th1, XBOOLE_1:28; ::_thesis: verum end; Lm3: for f being non constant standard special_circular_sequence holds ( Cl (Down ((LeftComp f),((L~ f) `))) is connected & Down ((LeftComp f),((L~ f) `)) = LeftComp f & Down ((LeftComp f),((L~ f) `)) is a_component ) proof let f be non constant standard special_circular_sequence; ::_thesis: ( Cl (Down ((LeftComp f),((L~ f) `))) is connected & Down ((LeftComp f),((L~ f) `)) = LeftComp f & Down ((LeftComp f),((L~ f) `)) is a_component ) LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def_1; then A1: ex B1 being Subset of ((TOP-REAL 2) | ((L~ f) `)) st ( B1 = LeftComp f & B1 is a_component ) by CONNSP_1:def_6; A2: the carrier of ((TOP-REAL 2) | ((L~ f) `)) = (L~ f) ` by PRE_TOPC:8; then Down ((LeftComp f),((L~ f) `)) = LeftComp f by A1, XBOOLE_1:28; then Down ((LeftComp f),((L~ f) `)) is connected by A1, CONNSP_1:def_5; hence Cl (Down ((LeftComp f),((L~ f) `))) is connected by CONNSP_1:19; ::_thesis: ( Down ((LeftComp f),((L~ f) `)) = LeftComp f & Down ((LeftComp f),((L~ f) `)) is a_component ) thus ( Down ((LeftComp f),((L~ f) `)) = LeftComp f & Down ((LeftComp f),((L~ f) `)) is a_component ) by A1, A2, XBOOLE_1:28; ::_thesis: verum end; Lm4: for f being non constant standard special_circular_sequence holds ( Cl (Down ((RightComp f),((L~ f) `))) is connected & Down ((RightComp f),((L~ f) `)) = RightComp f & Down ((RightComp f),((L~ f) `)) is a_component ) proof let f be non constant standard special_circular_sequence; ::_thesis: ( Cl (Down ((RightComp f),((L~ f) `))) is connected & Down ((RightComp f),((L~ f) `)) = RightComp f & Down ((RightComp f),((L~ f) `)) is a_component ) RightComp f is_a_component_of (L~ f) ` by GOBOARD9:def_2; then A1: ex B1 being Subset of ((TOP-REAL 2) | ((L~ f) `)) st ( B1 = RightComp f & B1 is a_component ) by CONNSP_1:def_6; A2: the carrier of ((TOP-REAL 2) | ((L~ f) `)) = (L~ f) ` by PRE_TOPC:8; then Down ((RightComp f),((L~ f) `)) = RightComp f by A1, XBOOLE_1:28; then Down ((RightComp f),((L~ f) `)) is connected by A1, CONNSP_1:def_5; hence Cl (Down ((RightComp f),((L~ f) `))) is connected by CONNSP_1:19; ::_thesis: ( Down ((RightComp f),((L~ f) `)) = RightComp f & Down ((RightComp f),((L~ f) `)) is a_component ) thus ( Down ((RightComp f),((L~ f) `)) = RightComp f & Down ((RightComp f),((L~ f) `)) is a_component ) by A1, A2, XBOOLE_1:28; ::_thesis: verum end; theorem Th4: :: GOBRD12:4 for f being non constant standard special_circular_sequence holds (L~ f) ` = union { (Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `)))) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } proof let f be non constant standard special_circular_sequence; ::_thesis: (L~ f) ` = union { (Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `)))) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } A1: the carrier of (TOP-REAL 2) = union { (cell ((GoB f),i,j)) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } by GOBRD11:7; A2: (L~ f) ` c= union { (Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `)))) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (L~ f) ` or x in union { (Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `)))) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } ) assume A3: x in (L~ f) ` ; ::_thesis: x in union { (Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `)))) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } then consider Y being set such that A4: ( x in Y & Y in { (cell ((GoB f),i,j)) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } ) by A1, TARSKI:def_4; consider i, j being Element of NAT such that A5: Y = cell ((GoB f),i,j) and A6: ( i <= len (GoB f) & j <= width (GoB f) ) by A4; reconsider Y0 = Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `))) as set ; x in (cell ((GoB f),i,j)) /\ ((L~ f) `) by A3, A4, A5, XBOOLE_0:def_4; then A7: x in Y0 by A6, Th2; Y0 in { (Cl (Down ((Int (cell ((GoB f),i1,j1))),((L~ f) `)))) where i1, j1 is Element of NAT : ( i1 <= len (GoB f) & j1 <= width (GoB f) ) } by A6; hence x in union { (Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `)))) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } by A7, TARSKI:def_4; ::_thesis: verum end; union { (Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `)))) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } c= (L~ f) ` proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union { (Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `)))) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } or x in (L~ f) ` ) assume x in union { (Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `)))) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } ; ::_thesis: x in (L~ f) ` then consider Y being set such that A8: ( x in Y & Y in { (Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `)))) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } ) by TARSKI:def_4; consider i, j being Element of NAT such that A9: Y = Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `))) and i <= len (GoB f) and j <= width (GoB f) by A8; Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `))) c= the carrier of ((TOP-REAL 2) | ((L~ f) `)) ; then Y c= (L~ f) ` by A9, Lm1; hence x in (L~ f) ` by A8; ::_thesis: verum end; hence (L~ f) ` = union { (Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `)))) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } by A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th5: :: GOBRD12:5 for f being non constant standard special_circular_sequence holds ( (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) is a_union_of_components of (TOP-REAL 2) | ((L~ f) `) & Down ((LeftComp f),((L~ f) `)) = LeftComp f & Down ((RightComp f),((L~ f) `)) = RightComp f ) proof let f be non constant standard special_circular_sequence; ::_thesis: ( (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) is a_union_of_components of (TOP-REAL 2) | ((L~ f) `) & Down ((LeftComp f),((L~ f) `)) = LeftComp f & Down ((RightComp f),((L~ f) `)) = RightComp f ) LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def_1; then consider B1 being Subset of ((TOP-REAL 2) | ((L~ f) `)) such that A1: B1 = LeftComp f and A2: B1 is a_component by CONNSP_1:def_6; RightComp f is_a_component_of (L~ f) ` by GOBOARD9:def_2; then consider B2 being Subset of ((TOP-REAL 2) | ((L~ f) `)) such that A3: B2 = RightComp f and A4: B2 is a_component by CONNSP_1:def_6; A5: B2 is Subset of ((L~ f) `) by Lm1; then A6: Down ((RightComp f),((L~ f) `)) is a_component by A3, A4, XBOOLE_1:28; A7: B1 is Subset of ((L~ f) `) by Lm1; then Down ((LeftComp f),((L~ f) `)) is a_component by A1, A2, XBOOLE_1:28; hence ( (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) is a_union_of_components of (TOP-REAL 2) | ((L~ f) `) & Down ((LeftComp f),((L~ f) `)) = LeftComp f & Down ((RightComp f),((L~ f) `)) = RightComp f ) by A1, A7, A3, A5, A6, GOBRD11:3, XBOOLE_1:28; ::_thesis: verum end; Lm5: for f being non constant standard special_circular_sequence for i1, j1, i2, j2 being Element of NAT st i1 <= len (GoB f) & j1 <= width (GoB f) & i2 <= len (GoB f) & j2 <= width (GoB f) & ( i2 = i1 + 1 or i1 = i2 + 1 ) & j1 = j2 & Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) holds Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) proof let f be non constant standard special_circular_sequence; ::_thesis: for i1, j1, i2, j2 being Element of NAT st i1 <= len (GoB f) & j1 <= width (GoB f) & i2 <= len (GoB f) & j2 <= width (GoB f) & ( i2 = i1 + 1 or i1 = i2 + 1 ) & j1 = j2 & Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) holds Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) let i1, j1, i2, j2 be Element of NAT ; ::_thesis: ( i1 <= len (GoB f) & j1 <= width (GoB f) & i2 <= len (GoB f) & j2 <= width (GoB f) & ( i2 = i1 + 1 or i1 = i2 + 1 ) & j1 = j2 & Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) implies Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) ) assume that A1: i1 <= len (GoB f) and A2: j1 <= width (GoB f) and A3: i2 <= len (GoB f) and A4: j2 <= width (GoB f) and A5: ( i2 = i1 + 1 or i1 = i2 + 1 ) and A6: j1 = j2 ; ::_thesis: ( not Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) or Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) ) now__::_thesis:_(_Int_(cell_((GoB_f),i1,j1))_c=_(LeftComp_f)_\/_(RightComp_f)_implies_Int_(cell_((GoB_f),i2,j2))_c=_(LeftComp_f)_\/_(RightComp_f)_) assume A7: Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) ; ::_thesis: Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) now__::_thesis:_(_(_i2_=_i1_+_1_&_Int_(cell_((GoB_f),i2,j2))_c=_(LeftComp_f)_\/_(RightComp_f)_)_or_(_i1_=_i2_+_1_&_Int_(cell_((GoB_f),i2,j2))_c=_(LeftComp_f)_\/_(RightComp_f)_)_) percases ( i2 = i1 + 1 or i1 = i2 + 1 ) by A5; caseA8: i2 = i1 + 1 ; ::_thesis: Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) now__::_thesis:_(_(_ex_k_being_Element_of_NAT_st_ (_1_<=_k_&_k_+_1_<=_len_f_&_j2_<>_0_&_j2_<>_width_(GoB_f)_&_LSeg_((f_/._k),(f_/._(k_+_1)))_=_LSeg_(((GoB_f)_*_((i1_+_1),j2)),((GoB_f)_*_((i1_+_1),(j2_+_1))))_)_&_Int_(cell_((GoB_f),(i1_+_1),j2))_c=_(LeftComp_f)_\/_(RightComp_f)_)_or_(_(_for_k_being_Element_of_NAT_holds_ (_not_1_<=_k_or_not_k_+_1_<=_len_f_or_not_j2_<>_0_or_not_j2_<>_width_(GoB_f)_or_not_LSeg_((f_/._k),(f_/._(k_+_1)))_=_LSeg_(((GoB_f)_*_((i1_+_1),j2)),((GoB_f)_*_((i1_+_1),(j2_+_1))))_)_)_&_Int_(cell_((GoB_f),(i1_+_1),j2))_c=_(LeftComp_f)_\/_(RightComp_f)_)_) percases ( ex k being Element of NAT st ( 1 <= k & k + 1 <= len f & j2 <> 0 & j2 <> width (GoB f) & LSeg ((f /. k),(f /. (k + 1))) = LSeg (((GoB f) * ((i1 + 1),j2)),((GoB f) * ((i1 + 1),(j2 + 1)))) ) or for k being Element of NAT holds ( not 1 <= k or not k + 1 <= len f or not j2 <> 0 or not j2 <> width (GoB f) or not LSeg ((f /. k),(f /. (k + 1))) = LSeg (((GoB f) * ((i1 + 1),j2)),((GoB f) * ((i1 + 1),(j2 + 1)))) ) ) ; case ex k being Element of NAT st ( 1 <= k & k + 1 <= len f & j2 <> 0 & j2 <> width (GoB f) & LSeg ((f /. k),(f /. (k + 1))) = LSeg (((GoB f) * ((i1 + 1),j2)),((GoB f) * ((i1 + 1),(j2 + 1)))) ) ; ::_thesis: Int (cell ((GoB f),(i1 + 1),j2)) c= (LeftComp f) \/ (RightComp f) then consider k being Element of NAT such that A9: ( 1 <= k & k + 1 <= len f ) and A10: j2 <> 0 and A11: j2 <> width (GoB f) and A12: LSeg ((f /. k),(f /. (k + 1))) = LSeg (((GoB f) * ((i1 + 1),j2)),((GoB f) * ((i1 + 1),(j2 + 1)))) ; now__::_thesis:_(_(_f_/._k_=_(GoB_f)_*_((i1_+_1),j2)_&_f_/._(k_+_1)_=_(GoB_f)_*_((i1_+_1),(j2_+_1))_&_Int_(cell_((GoB_f),(i1_+_1),j2))_c=_(LeftComp_f)_\/_(RightComp_f)_)_or_(_f_/._k_=_(GoB_f)_*_((i1_+_1),(j2_+_1))_&_f_/._(k_+_1)_=_(GoB_f)_*_((i1_+_1),j2)_&_Int_(cell_((GoB_f),(i1_+_1),j2))_c=_(LeftComp_f)_\/_(RightComp_f)_)_) percases ( ( f /. k = (GoB f) * ((i1 + 1),j2) & f /. (k + 1) = (GoB f) * ((i1 + 1),(j2 + 1)) ) or ( f /. k = (GoB f) * ((i1 + 1),(j2 + 1)) & f /. (k + 1) = (GoB f) * ((i1 + 1),j2) ) ) by A12, SPPOL_1:8; caseA13: ( f /. k = (GoB f) * ((i1 + 1),j2) & f /. (k + 1) = (GoB f) * ((i1 + 1),(j2 + 1)) ) ; ::_thesis: Int (cell ((GoB f),(i1 + 1),j2)) c= (LeftComp f) \/ (RightComp f) A14: ( Int (right_cell (f,k)) c= RightComp f & RightComp f c= (LeftComp f) \/ (RightComp f) ) by A9, GOBOARD9:25, XBOOLE_1:7; j2 < width (GoB f) by A4, A11, XXREAL_0:1; then A15: j2 + 1 <= width (GoB f) by NAT_1:13; 0 + 1 <= i1 + 1 by XREAL_1:6; then A16: ( Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] & i1 + 1 in dom (GoB f) ) by A3, A8, FINSEQ_3:25, MATRIX_1:def_4; 1 <= j2 + 1 by NAT_1:11; then j2 + 1 in Seg (width (GoB f)) by A15, FINSEQ_1:1; then A17: [(i1 + 1),(j2 + 1)] in Indices (GoB f) by A16, ZFMISC_1:87; j2 >= 0 + 1 by A10, NAT_1:13; then j2 in Seg (width (GoB f)) by A4, FINSEQ_1:1; then [(i1 + 1),j2] in Indices (GoB f) by A16, ZFMISC_1:87; then right_cell (f,k) = cell ((GoB f),(i1 + 1),j2) by A9, A13, A17, GOBOARD5:27; hence Int (cell ((GoB f),(i1 + 1),j2)) c= (LeftComp f) \/ (RightComp f) by A14, XBOOLE_1:1; ::_thesis: verum end; caseA18: ( f /. k = (GoB f) * ((i1 + 1),(j2 + 1)) & f /. (k + 1) = (GoB f) * ((i1 + 1),j2) ) ; ::_thesis: Int (cell ((GoB f),(i1 + 1),j2)) c= (LeftComp f) \/ (RightComp f) A19: ( Int (left_cell (f,k)) c= LeftComp f & LeftComp f c= (LeftComp f) \/ (RightComp f) ) by A9, GOBOARD9:21, XBOOLE_1:7; j2 < width (GoB f) by A4, A11, XXREAL_0:1; then A20: j2 + 1 <= width (GoB f) by NAT_1:13; 0 + 1 <= i1 + 1 by XREAL_1:6; then A21: ( Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] & i1 + 1 in dom (GoB f) ) by A3, A8, FINSEQ_3:25, MATRIX_1:def_4; 1 <= j2 + 1 by NAT_1:11; then j2 + 1 in Seg (width (GoB f)) by A20, FINSEQ_1:1; then A22: [(i1 + 1),(j2 + 1)] in Indices (GoB f) by A21, ZFMISC_1:87; j2 >= 0 + 1 by A10, NAT_1:13; then j2 in Seg (width (GoB f)) by A4, FINSEQ_1:1; then [(i1 + 1),j2] in Indices (GoB f) by A21, ZFMISC_1:87; then left_cell (f,k) = cell ((GoB f),(i1 + 1),j2) by A9, A18, A22, GOBOARD5:30; hence Int (cell ((GoB f),(i1 + 1),j2)) c= (LeftComp f) \/ (RightComp f) by A19, XBOOLE_1:1; ::_thesis: verum end; end; end; hence Int (cell ((GoB f),(i1 + 1),j2)) c= (LeftComp f) \/ (RightComp f) ; ::_thesis: verum end; caseA23: for k being Element of NAT holds ( not 1 <= k or not k + 1 <= len f or not j2 <> 0 or not j2 <> width (GoB f) or not LSeg ((f /. k),(f /. (k + 1))) = LSeg (((GoB f) * ((i1 + 1),j2)),((GoB f) * ((i1 + 1),(j2 + 1)))) ) ; ::_thesis: Int (cell ((GoB f),(i1 + 1),j2)) c= (LeftComp f) \/ (RightComp f) now__::_thesis:_(_(_j2_=_0_&_Int_(cell_((GoB_f),(i1_+_1),j2))_c=_(LeftComp_f)_\/_(RightComp_f)_)_or_(_j2_=_width_(GoB_f)_&_Int_(cell_((GoB_f),(i1_+_1),j2))_c=_(LeftComp_f)_\/_(RightComp_f)_)_or_(_j2_<>_0_&_j2_<>_width_(GoB_f)_&_(_for_k_being_Element_of_NAT_holds_ (_not_1_<=_k_or_not_k_+_1_<=_len_f_or_not_LSeg_((f_/._k),(f_/._(k_+_1)))_=_LSeg_(((GoB_f)_*_((i1_+_1),j2)),((GoB_f)_*_((i1_+_1),(j2_+_1))))_)_)_&_Int_(cell_((GoB_f),(i1_+_1),j2))_c=_(LeftComp_f)_\/_(RightComp_f)_)_) percases ( j2 = 0 or j2 = width (GoB f) or ( j2 <> 0 & j2 <> width (GoB f) & ( for k being Element of NAT holds ( not 1 <= k or not k + 1 <= len f or not LSeg ((f /. k),(f /. (k + 1))) = LSeg (((GoB f) * ((i1 + 1),j2)),((GoB f) * ((i1 + 1),(j2 + 1)))) ) ) ) ) by A23; caseA24: j2 = 0 ; ::_thesis: Int (cell ((GoB f),(i1 + 1),j2)) c= (LeftComp f) \/ (RightComp f) reconsider p = |[(((GoB f) * ((i1 + 1),1)) `1),((((GoB f) * ((i1 + 1),1)) `2) - 1)]| as Point of (TOP-REAL 2) ; A25: 1 < width (GoB f) by GOBOARD7:33; A26: 1 < len (GoB f) by GOBOARD7:32; reconsider P = {p} as Subset of (TOP-REAL 2) ; A27: p `2 < (p `2) + 1 by XREAL_1:29; A28: 1 <= i1 + 1 by NAT_1:11; then ((GoB f) * ((i1 + 1),1)) `2 = ((GoB f) * (1,1)) `2 by A3, A8, A25, GOBOARD5:1; then A29: p `2 = (((GoB f) * (1,1)) `2) - 1 by EUCLID:52; p in { |[r,s]| where r, s is Real : s <= ((GoB f) * (1,1)) `2 } proof p = |[(p `1),(p `2)]| by EUCLID:53; hence p in { |[r,s]| where r, s is Real : s <= ((GoB f) * (1,1)) `2 } by A29, A27; ::_thesis: verum end; then A30: p in h_strip ((GoB f),j2) by A24, A26, GOBOARD5:7; ( ( for q being Point of (TOP-REAL 2) st q in P holds q `2 < ((GoB f) * (1,1)) `2 ) implies P misses L~ f ) by GOBOARD8:23; then A31: ( p in {p} & {p} c= (L~ f) ` ) by A29, A27, SUBSET_1:23, TARSKI:def_1; then reconsider p1 = p as Point of ((TOP-REAL 2) | ((L~ f) `)) by PRE_TOPC:8; A32: ( i1 = 0 or i1 >= 0 + 1 ) by NAT_1:13; A33: now__::_thesis:_(_(_i1_>=_1_&_i1_+_1_<_len_(GoB_f)_&_p_in_(cell_((GoB_f),(i1_+_1),j2))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i1,j2))_/\_((L~_f)_`)_)_or_(_i1_>=_1_&_i1_+_1_=_len_(GoB_f)_&_p_in_(cell_((GoB_f),(i1_+_1),j2))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i1,j2))_/\_((L~_f)_`)_)_or_(_i1_=_0_&_i1_+_1_<_len_(GoB_f)_&_p_in_(cell_((GoB_f),(i1_+_1),j2))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i1,j2))_/\_((L~_f)_`)_)_or_(_i1_=_0_&_i1_+_1_=_len_(GoB_f)_&_p_in_(cell_((GoB_f),(i1_+_1),j2))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i1,j2))_/\_((L~_f)_`)_)_) percases ( ( i1 >= 1 & i1 + 1 < len (GoB f) ) or ( i1 >= 1 & i1 + 1 = len (GoB f) ) or ( i1 = 0 & i1 + 1 < len (GoB f) ) or ( i1 = 0 & i1 + 1 = len (GoB f) ) ) by A3, A8, A32, XXREAL_0:1; caseA34: ( i1 >= 1 & i1 + 1 < len (GoB f) ) ; ::_thesis: ( p in (cell ((GoB f),(i1 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i1,j2)) /\ ((L~ f) `) ) then A35: (i1 + 1) + 1 <= len (GoB f) by NAT_1:13; A36: p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i1 + 1),1)) `1 <= r & r <= ((GoB f) * (((i1 + 1) + 1),1)) `1 ) } proof i1 + 1 < (i1 + 1) + 1 by NAT_1:13; then ((GoB f) * ((i1 + 1),1)) `1 <= ((GoB f) * (((i1 + 1) + 1),1)) `1 by A25, A28, A35, GOBOARD5:3; hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i1 + 1),1)) `1 <= r & r <= ((GoB f) * (((i1 + 1) + 1),1)) `1 ) } ; ::_thesis: verum end; 1 <= i1 + 1 by NAT_1:11; then p in v_strip ((GoB f),(i1 + 1)) by A25, A34, A36, GOBOARD5:8; then p in (v_strip ((GoB f),(i1 + 1))) /\ (h_strip ((GoB f),j2)) by A30, XBOOLE_0:def_4; then A37: p in cell ((GoB f),(i1 + 1),j2) by GOBOARD5:def_3; A38: p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i1,1)) `1 <= r & r <= ((GoB f) * ((i1 + 1),1)) `1 ) } proof i1 < i1 + 1 by NAT_1:13; then ((GoB f) * (i1,1)) `1 < ((GoB f) * ((i1 + 1),1)) `1 by A25, A34, GOBOARD5:3; hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i1,1)) `1 <= r & r <= ((GoB f) * ((i1 + 1),1)) `1 ) } ; ::_thesis: verum end; i1 < len (GoB f) by A34, NAT_1:13; then p in v_strip ((GoB f),i1) by A25, A34, A38, GOBOARD5:8; then p in (v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j2)) by A30, XBOOLE_0:def_4; then p in cell ((GoB f),i1,j2) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),(i1 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i1,j2)) /\ ((L~ f) `) ) by A31, A37, XBOOLE_0:def_4; ::_thesis: verum end; caseA39: ( i1 >= 1 & i1 + 1 = len (GoB f) ) ; ::_thesis: ( p in (cell ((GoB f),(i1 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i1,j2)) /\ ((L~ f) `) ) A40: i1 < i1 + 1 by NAT_1:13; A41: p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i1,1)) `1 <= r & r <= ((GoB f) * ((i1 + 1),1)) `1 ) } proof ((GoB f) * (i1,1)) `1 < ((GoB f) * ((i1 + 1),1)) `1 by A25, A39, A40, GOBOARD5:3; hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i1,1)) `1 <= r & r <= ((GoB f) * ((i1 + 1),1)) `1 ) } ; ::_thesis: verum end; p in { |[r,s]| where r, s is Real : ((GoB f) * ((i1 + 1),1)) `1 <= r } ; then p in v_strip ((GoB f),(i1 + 1)) by A25, A39, GOBOARD5:9; then p in (v_strip ((GoB f),(i1 + 1))) /\ (h_strip ((GoB f),j2)) by A30, XBOOLE_0:def_4; then A42: p in cell ((GoB f),(i1 + 1),j2) by GOBOARD5:def_3; i1 < len (GoB f) by A39, NAT_1:13; then p in v_strip ((GoB f),i1) by A25, A39, A41, GOBOARD5:8; then p in (v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j2)) by A30, XBOOLE_0:def_4; then p in cell ((GoB f),i1,j2) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),(i1 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i1,j2)) /\ ((L~ f) `) ) by A31, A42, XBOOLE_0:def_4; ::_thesis: verum end; caseA43: ( i1 = 0 & i1 + 1 < len (GoB f) ) ; ::_thesis: ( p in (cell ((GoB f),(i1 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i1,j2)) /\ ((L~ f) `) ) then A44: (i1 + 1) + 1 <= len (GoB f) by NAT_1:13; p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i1 + 1),1)) `1 <= r & r <= ((GoB f) * (((i1 + 1) + 1),1)) `1 ) } proof i1 + 1 < (i1 + 1) + 1 by NAT_1:13; then ((GoB f) * ((i1 + 1),1)) `1 <= ((GoB f) * (((i1 + 1) + 1),1)) `1 by A25, A28, A44, GOBOARD5:3; hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i1 + 1),1)) `1 <= r & r <= ((GoB f) * (((i1 + 1) + 1),1)) `1 ) } ; ::_thesis: verum end; then p in v_strip ((GoB f),(i1 + 1)) by A25, A43, GOBOARD5:8; then p in (v_strip ((GoB f),(i1 + 1))) /\ (h_strip ((GoB f),j2)) by A30, XBOOLE_0:def_4; then A45: p in cell ((GoB f),(i1 + 1),j2) by GOBOARD5:def_3; p in { |[r,s]| where r, s is Real : r <= ((GoB f) * (1,1)) `1 } by A43; then p in v_strip ((GoB f),i1) by A25, A43, GOBOARD5:10; then p in (v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j2)) by A30, XBOOLE_0:def_4; then p in cell ((GoB f),i1,j2) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),(i1 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i1,j2)) /\ ((L~ f) `) ) by A31, A45, XBOOLE_0:def_4; ::_thesis: verum end; caseA46: ( i1 = 0 & i1 + 1 = len (GoB f) ) ; ::_thesis: ( p in (cell ((GoB f),(i1 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i1,j2)) /\ ((L~ f) `) ) p in { |[r,s]| where r, s is Real : ((GoB f) * ((i1 + 1),1)) `1 <= r } ; then p in v_strip ((GoB f),(i1 + 1)) by A25, A46, GOBOARD5:9; then p in (v_strip ((GoB f),(i1 + 1))) /\ (h_strip ((GoB f),j2)) by A30, XBOOLE_0:def_4; then A47: p in cell ((GoB f),(i1 + 1),j2) by GOBOARD5:def_3; p in { |[r,s]| where r, s is Real : r <= ((GoB f) * (1,1)) `1 } by A46; then p in v_strip ((GoB f),i1) by A25, A46, GOBOARD5:10; then p in (v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j2)) by A30, XBOOLE_0:def_4; then p in cell ((GoB f),i1,j2) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),(i1 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i1,j2)) /\ ((L~ f) `) ) by A31, A47, XBOOLE_0:def_4; ::_thesis: verum end; end; end; then p in Cl (Down ((Int (cell ((GoB f),(i1 + 1),j2))),((L~ f) `))) by A4, Th2; then A48: Cl (Down ((Int (cell ((GoB f),(i1 + 1),j2))),((L~ f) `))) c= Component_of p1 by A3, A4, A8, Th3, GOBRD11:1; Down ((RightComp f),((L~ f) `)) is closed by Lm4, CONNSP_1:33; then A49: Cl (Down ((RightComp f),((L~ f) `))) = Down ((RightComp f),((L~ f) `)) by PRE_TOPC:22; Down ((LeftComp f),((L~ f) `)) is closed by Lm3, CONNSP_1:33; then A50: Cl (Down ((LeftComp f),((L~ f) `))) = Down ((LeftComp f),((L~ f) `)) by PRE_TOPC:22; (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) = Down (((LeftComp f) \/ (RightComp f)),((L~ f) `)) by GOBRD11:4; then A51: Cl (Down (((LeftComp f) \/ (RightComp f)),((L~ f) `))) = (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A50, A49, PRE_TOPC:20; A52: ( Down ((Int (cell ((GoB f),(i1 + 1),j2))),((L~ f) `)) c= Cl (Down ((Int (cell ((GoB f),(i1 + 1),j2))),((L~ f) `))) & Down ((Int (cell ((GoB f),(i1 + 1),j2))),((L~ f) `)) = Int (cell ((GoB f),(i1 + 1),j2)) ) by A3, A4, A8, Th3, PRE_TOPC:18; A53: ( Down ((LeftComp f),((L~ f) `)) = LeftComp f & Down ((RightComp f),((L~ f) `)) = RightComp f ) by Th5; Down ((Int (cell ((GoB f),i1,j2))),((L~ f) `)) c= (LeftComp f) \/ (RightComp f) by A1, A2, A6, A7, Th3; then Down ((Int (cell ((GoB f),i1,j2))),((L~ f) `)) c= Down (((LeftComp f) \/ (RightComp f)),((L~ f) `)) by A53, GOBRD11:4; then A54: Cl (Down ((Int (cell ((GoB f),i1,j2))),((L~ f) `))) c= Cl (Down (((LeftComp f) \/ (RightComp f)),((L~ f) `))) by PRE_TOPC:19; p in Cl (Down ((Int (cell ((GoB f),i1,j2))),((L~ f) `))) by A1, A4, A33, Th2; then Component_of p1 c= (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A54, A51, Th5, CONNSP_3:21; then Cl (Down ((Int (cell ((GoB f),(i1 + 1),j2))),((L~ f) `))) c= (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A48, XBOOLE_1:1; hence Int (cell ((GoB f),(i1 + 1),j2)) c= (LeftComp f) \/ (RightComp f) by A53, A52, XBOOLE_1:1; ::_thesis: verum end; caseA55: j2 = width (GoB f) ; ::_thesis: Int (cell ((GoB f),(i1 + 1),j2)) c= (LeftComp f) \/ (RightComp f) reconsider p = |[(((GoB f) * ((i1 + 1),(width (GoB f)))) `1),((((GoB f) * ((i1 + 1),(width (GoB f)))) `2) + 1)]| as Point of (TOP-REAL 2) ; A56: 1 < width (GoB f) by GOBOARD7:33; reconsider P = {p} as Subset of (TOP-REAL 2) ; A57: ( ( for q being Point of (TOP-REAL 2) st q in P holds ((GoB f) * (1,(width (GoB f)))) `2 < q `2 ) implies P misses L~ f ) by GOBOARD8:24; A58: 1 < len (GoB f) by GOBOARD7:32; A59: 1 <= 1 + i1 by NAT_1:11; then ((GoB f) * ((i1 + 1),(width (GoB f)))) `2 = ((GoB f) * (1,(width (GoB f)))) `2 by A3, A8, A56, GOBOARD5:1; then A60: p `2 = (((GoB f) * (1,(width (GoB f)))) `2) + 1 by EUCLID:52; then A61: ((GoB f) * (1,(width (GoB f)))) `2 < p `2 by XREAL_1:29; p in { |[r,s]| where r, s is Real : ((GoB f) * (1,(width (GoB f)))) `2 <= s } proof p = |[(p `1),(p `2)]| by EUCLID:53; hence p in { |[r,s]| where r, s is Real : ((GoB f) * (1,(width (GoB f)))) `2 <= s } by A61; ::_thesis: verum end; then A62: p in h_strip ((GoB f),j2) by A55, A58, GOBOARD5:6; ((GoB f) * (1,(width (GoB f)))) `2 < (((GoB f) * (1,(width (GoB f)))) `2) + 1 by XREAL_1:29; then A63: ( p in {p} & {p} c= (L~ f) ` ) by A60, A57, SUBSET_1:23, TARSKI:def_1; then reconsider p1 = p as Point of ((TOP-REAL 2) | ((L~ f) `)) by PRE_TOPC:8; A64: ( i1 = 0 or i1 >= 0 + 1 ) by NAT_1:13; A65: now__::_thesis:_(_(_i1_>=_1_&_i1_+_1_<_len_(GoB_f)_&_p_in_(cell_((GoB_f),(i1_+_1),j2))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i1,j2))_/\_((L~_f)_`)_)_or_(_i1_>=_1_&_i1_+_1_=_len_(GoB_f)_&_p_in_(cell_((GoB_f),(i1_+_1),j2))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i1,j2))_/\_((L~_f)_`)_)_or_(_i1_=_0_&_i1_+_1_<_len_(GoB_f)_&_p_in_(cell_((GoB_f),(i1_+_1),j2))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i1,j2))_/\_((L~_f)_`)_)_or_(_i1_=_0_&_i1_+_1_=_len_(GoB_f)_&_contradiction_)_) percases ( ( i1 >= 1 & i1 + 1 < len (GoB f) ) or ( i1 >= 1 & i1 + 1 = len (GoB f) ) or ( i1 = 0 & i1 + 1 < len (GoB f) ) or ( i1 = 0 & i1 + 1 = len (GoB f) ) ) by A3, A8, A64, XXREAL_0:1; caseA66: ( i1 >= 1 & i1 + 1 < len (GoB f) ) ; ::_thesis: ( p in (cell ((GoB f),(i1 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i1,j2)) /\ ((L~ f) `) ) then A67: (i1 + 1) + 1 <= len (GoB f) by NAT_1:13; A68: p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i1 + 1),(width (GoB f)))) `1 <= r & r <= ((GoB f) * (((i1 + 1) + 1),(width (GoB f)))) `1 ) } proof i1 + 1 < (i1 + 1) + 1 by NAT_1:13; then ((GoB f) * ((i1 + 1),(width (GoB f)))) `1 <= ((GoB f) * (((i1 + 1) + 1),(width (GoB f)))) `1 by A56, A59, A67, GOBOARD5:3; hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i1 + 1),(width (GoB f)))) `1 <= r & r <= ((GoB f) * (((i1 + 1) + 1),(width (GoB f)))) `1 ) } ; ::_thesis: verum end; 1 <= i1 + 1 by NAT_1:11; then p in v_strip ((GoB f),(i1 + 1)) by A56, A66, A68, GOBOARD5:8; then p in (v_strip ((GoB f),(i1 + 1))) /\ (h_strip ((GoB f),j2)) by A62, XBOOLE_0:def_4; then A69: p in cell ((GoB f),(i1 + 1),j2) by GOBOARD5:def_3; A70: p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i1,(width (GoB f)))) `1 <= r & r <= ((GoB f) * ((i1 + 1),(width (GoB f)))) `1 ) } proof i1 < i1 + 1 by NAT_1:13; then ((GoB f) * (i1,(width (GoB f)))) `1 < ((GoB f) * ((i1 + 1),(width (GoB f)))) `1 by A56, A66, GOBOARD5:3; hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i1,(width (GoB f)))) `1 <= r & r <= ((GoB f) * ((i1 + 1),(width (GoB f)))) `1 ) } ; ::_thesis: verum end; i1 < len (GoB f) by A66, NAT_1:13; then p in v_strip ((GoB f),i1) by A56, A66, A70, GOBOARD5:8; then p in (v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j2)) by A62, XBOOLE_0:def_4; then p in cell ((GoB f),i1,j2) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),(i1 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i1,j2)) /\ ((L~ f) `) ) by A63, A69, XBOOLE_0:def_4; ::_thesis: verum end; caseA71: ( i1 >= 1 & i1 + 1 = len (GoB f) ) ; ::_thesis: ( p in (cell ((GoB f),(i1 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i1,j2)) /\ ((L~ f) `) ) A72: i1 < i1 + 1 by NAT_1:13; A73: p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i1,(width (GoB f)))) `1 <= r & r <= ((GoB f) * ((i1 + 1),(width (GoB f)))) `1 ) } proof ((GoB f) * (i1,(width (GoB f)))) `1 < ((GoB f) * ((i1 + 1),(width (GoB f)))) `1 by A56, A71, A72, GOBOARD5:3; hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i1,(width (GoB f)))) `1 <= r & r <= ((GoB f) * ((i1 + 1),(width (GoB f)))) `1 ) } ; ::_thesis: verum end; p in { |[r,s]| where r, s is Real : ((GoB f) * ((i1 + 1),(width (GoB f)))) `1 <= r } ; then p in v_strip ((GoB f),(i1 + 1)) by A56, A71, GOBOARD5:9; then p in (v_strip ((GoB f),(i1 + 1))) /\ (h_strip ((GoB f),j2)) by A62, XBOOLE_0:def_4; then A74: p in cell ((GoB f),(i1 + 1),j2) by GOBOARD5:def_3; i1 < len (GoB f) by A71, NAT_1:13; then p in v_strip ((GoB f),i1) by A56, A71, A73, GOBOARD5:8; then p in (v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j2)) by A62, XBOOLE_0:def_4; then p in cell ((GoB f),i1,j2) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),(i1 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i1,j2)) /\ ((L~ f) `) ) by A63, A74, XBOOLE_0:def_4; ::_thesis: verum end; caseA75: ( i1 = 0 & i1 + 1 < len (GoB f) ) ; ::_thesis: ( p in (cell ((GoB f),(i1 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i1,j2)) /\ ((L~ f) `) ) then A76: (i1 + 1) + 1 <= len (GoB f) by NAT_1:13; p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i1 + 1),(width (GoB f)))) `1 <= r & r <= ((GoB f) * (((i1 + 1) + 1),(width (GoB f)))) `1 ) } proof i1 + 1 < (i1 + 1) + 1 by NAT_1:13; then ((GoB f) * ((i1 + 1),(width (GoB f)))) `1 <= ((GoB f) * (((i1 + 1) + 1),(width (GoB f)))) `1 by A56, A59, A76, GOBOARD5:3; hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i1 + 1),(width (GoB f)))) `1 <= r & r <= ((GoB f) * (((i1 + 1) + 1),(width (GoB f)))) `1 ) } ; ::_thesis: verum end; then p in v_strip ((GoB f),(i1 + 1)) by A56, A75, GOBOARD5:8; then p in (v_strip ((GoB f),(i1 + 1))) /\ (h_strip ((GoB f),j2)) by A62, XBOOLE_0:def_4; then A77: p in cell ((GoB f),(i1 + 1),j2) by GOBOARD5:def_3; p in { |[r,s]| where r, s is Real : r <= ((GoB f) * (1,(width (GoB f)))) `1 } by A75; then p in v_strip ((GoB f),i1) by A56, A75, GOBOARD5:10; then p in (v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j2)) by A62, XBOOLE_0:def_4; then p in cell ((GoB f),i1,j2) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),(i1 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i1,j2)) /\ ((L~ f) `) ) by A63, A77, XBOOLE_0:def_4; ::_thesis: verum end; case ( i1 = 0 & i1 + 1 = len (GoB f) ) ; ::_thesis: contradiction hence contradiction by GOBOARD7:32; ::_thesis: verum end; end; end; then p in Cl (Down ((Int (cell ((GoB f),(i1 + 1),j2))),((L~ f) `))) by A4, Th2; then A78: Cl (Down ((Int (cell ((GoB f),(i1 + 1),j2))),((L~ f) `))) c= Component_of p1 by A3, A4, A8, Th3, GOBRD11:1; Down ((RightComp f),((L~ f) `)) is closed by Lm4, CONNSP_1:33; then A79: Cl (Down ((RightComp f),((L~ f) `))) = Down ((RightComp f),((L~ f) `)) by PRE_TOPC:22; Down ((LeftComp f),((L~ f) `)) is closed by Lm3, CONNSP_1:33; then A80: Cl (Down ((LeftComp f),((L~ f) `))) = Down ((LeftComp f),((L~ f) `)) by PRE_TOPC:22; (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) = Down (((LeftComp f) \/ (RightComp f)),((L~ f) `)) by GOBRD11:4; then A81: Cl (Down (((LeftComp f) \/ (RightComp f)),((L~ f) `))) = (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A80, A79, PRE_TOPC:20; A82: ( Down ((Int (cell ((GoB f),(i1 + 1),j2))),((L~ f) `)) c= Cl (Down ((Int (cell ((GoB f),(i1 + 1),j2))),((L~ f) `))) & Down ((Int (cell ((GoB f),(i1 + 1),j2))),((L~ f) `)) = Int (cell ((GoB f),(i1 + 1),j2)) ) by A3, A4, A8, Th3, PRE_TOPC:18; A83: ( Down ((LeftComp f),((L~ f) `)) = LeftComp f & Down ((RightComp f),((L~ f) `)) = RightComp f ) by Th5; Down ((Int (cell ((GoB f),i1,j2))),((L~ f) `)) c= (LeftComp f) \/ (RightComp f) by A1, A2, A6, A7, Th3; then Down ((Int (cell ((GoB f),i1,j2))),((L~ f) `)) c= Down (((LeftComp f) \/ (RightComp f)),((L~ f) `)) by A83, GOBRD11:4; then A84: Cl (Down ((Int (cell ((GoB f),i1,j2))),((L~ f) `))) c= Cl (Down (((LeftComp f) \/ (RightComp f)),((L~ f) `))) by PRE_TOPC:19; p in Cl (Down ((Int (cell ((GoB f),i1,j2))),((L~ f) `))) by A1, A4, A65, Th2; then Component_of p1 c= (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A84, A81, Th5, CONNSP_3:21; then Cl (Down ((Int (cell ((GoB f),(i1 + 1),j2))),((L~ f) `))) c= (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A78, XBOOLE_1:1; hence Int (cell ((GoB f),(i1 + 1),j2)) c= (LeftComp f) \/ (RightComp f) by A83, A82, XBOOLE_1:1; ::_thesis: verum end; caseA85: ( j2 <> 0 & j2 <> width (GoB f) & ( for k being Element of NAT holds ( not 1 <= k or not k + 1 <= len f or not LSeg ((f /. k),(f /. (k + 1))) = LSeg (((GoB f) * ((i1 + 1),j2)),((GoB f) * ((i1 + 1),(j2 + 1)))) ) ) ) ; ::_thesis: Int (cell ((GoB f),(i1 + 1),j2)) c= (LeftComp f) \/ (RightComp f) then A86: j2 < width (GoB f) by A4, XXREAL_0:1; then A87: j2 + 1 <= width (GoB f) by NAT_1:13; for k being Element of NAT st 1 <= k & k + 1 <= len f holds LSeg (((GoB f) * ((i1 + 1),j2)),((GoB f) * ((i1 + 1),(j2 + 1)))) <> LSeg (f,k) proof let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f implies LSeg (((GoB f) * ((i1 + 1),j2)),((GoB f) * ((i1 + 1),(j2 + 1)))) <> LSeg (f,k) ) assume A88: ( 1 <= k & k + 1 <= len f ) ; ::_thesis: LSeg (((GoB f) * ((i1 + 1),j2)),((GoB f) * ((i1 + 1),(j2 + 1)))) <> LSeg (f,k) then LSeg (f,k) = LSeg ((f /. k),(f /. (k + 1))) by TOPREAL1:def_3; hence LSeg (((GoB f) * ((i1 + 1),j2)),((GoB f) * ((i1 + 1),(j2 + 1)))) <> LSeg (f,k) by A85, A88; ::_thesis: verum end; then A89: ( 1 <= i1 + 1 & i1 + 1 <= len (GoB f) & 1 <= j2 & j2 + 1 <= width (GoB f) implies not (1 / 2) * (((GoB f) * ((i1 + 1),j2)) + ((GoB f) * ((i1 + 1),(j2 + 1)))) in L~ f ) by GOBOARD7:39; reconsider p = (1 / 2) * (((GoB f) * ((i1 + 1),j2)) + ((GoB f) * ((i1 + 1),(j2 + 1)))) as Point of (TOP-REAL 2) ; A90: p `2 = (1 / 2) * ((((GoB f) * ((i1 + 1),j2)) + ((GoB f) * ((i1 + 1),(j2 + 1)))) `2) by TOPREAL3:4 .= (1 / 2) * ((((GoB f) * ((i1 + 1),j2)) `2) + (((GoB f) * ((i1 + 1),(j2 + 1))) `2)) by TOPREAL3:2 ; reconsider P = {p} as Subset of (TOP-REAL 2) ; A91: 1 < width (GoB f) by GOBOARD7:33; Down ((RightComp f),((L~ f) `)) is closed by Lm4, CONNSP_1:33; then A92: Cl (Down ((RightComp f),((L~ f) `))) = Down ((RightComp f),((L~ f) `)) by PRE_TOPC:22; Down ((LeftComp f),((L~ f) `)) is closed by Lm3, CONNSP_1:33; then A93: Cl (Down ((LeftComp f),((L~ f) `))) = Down ((LeftComp f),((L~ f) `)) by PRE_TOPC:22; (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) = Down (((LeftComp f) \/ (RightComp f)),((L~ f) `)) by GOBRD11:4; then A94: Cl (Down (((LeftComp f) \/ (RightComp f)),((L~ f) `))) = (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A93, A92, PRE_TOPC:20; A95: ( Down ((LeftComp f),((L~ f) `)) = LeftComp f & Down ((RightComp f),((L~ f) `)) = RightComp f ) by Th5; Down ((Int (cell ((GoB f),i1,j2))),((L~ f) `)) c= (LeftComp f) \/ (RightComp f) by A1, A2, A6, A7, Th3; then Down ((Int (cell ((GoB f),i1,j2))),((L~ f) `)) c= Down (((LeftComp f) \/ (RightComp f)),((L~ f) `)) by A95, GOBRD11:4; then A96: Cl (Down ((Int (cell ((GoB f),i1,j2))),((L~ f) `))) c= Cl (Down (((LeftComp f) \/ (RightComp f)),((L~ f) `))) by PRE_TOPC:19; A97: ( Down ((Int (cell ((GoB f),(i1 + 1),j2))),((L~ f) `)) c= Cl (Down ((Int (cell ((GoB f),(i1 + 1),j2))),((L~ f) `))) & Down ((Int (cell ((GoB f),(i1 + 1),j2))),((L~ f) `)) = Int (cell ((GoB f),(i1 + 1),j2)) ) by A3, A4, A8, Th3, PRE_TOPC:18; A98: 1 <= i1 + 1 by NAT_1:11; A99: 0 + 1 <= j2 by A85, NAT_1:13; then A100: 1 < j2 + 1 by NAT_1:13; ( ( for x being set st x in P holds not x in L~ f ) implies P misses L~ f ) by XBOOLE_0:3; then A101: ( p in {p} & {p} c= (L~ f) ` ) by A3, A8, A99, A86, A89, NAT_1:13, SUBSET_1:23, TARSKI:def_1; then reconsider p1 = p as Point of ((TOP-REAL 2) | ((L~ f) `)) by PRE_TOPC:8; A102: 1 <= 1 + i1 by NAT_1:11; p `1 = (1 / 2) * ((((GoB f) * ((i1 + 1),j2)) + ((GoB f) * ((i1 + 1),(j2 + 1)))) `1) by TOPREAL3:4 .= (1 / 2) * ((((GoB f) * ((i1 + 1),j2)) `1) + (((GoB f) * ((i1 + 1),(j2 + 1))) `1)) by TOPREAL3:2 ; then A103: p = |[((1 / 2) * ((((GoB f) * ((i1 + 1),j2)) `1) + (((GoB f) * ((i1 + 1),(j2 + 1))) `1))),((1 / 2) * ((((GoB f) * ((i1 + 1),j2)) `2) + (((GoB f) * ((i1 + 1),(j2 + 1))) `2)))]| by A90, EUCLID:53; j2 < j2 + 1 by NAT_1:13; then A104: ((GoB f) * ((i1 + 1),j2)) `2 < ((GoB f) * ((i1 + 1),(j2 + 1))) `2 by A3, A8, A99, A87, A102, GOBOARD5:4; then (((GoB f) * ((i1 + 1),j2)) `2) + (((GoB f) * ((i1 + 1),(j2 + 1))) `2) < (((GoB f) * ((i1 + 1),(j2 + 1))) `2) + (((GoB f) * ((i1 + 1),(j2 + 1))) `2) by XREAL_1:8; then A105: ((((GoB f) * ((i1 + 1),j2)) `2) + (((GoB f) * ((i1 + 1),(j2 + 1))) `2)) / 2 < ((((GoB f) * ((i1 + 1),(j2 + 1))) `2) + (((GoB f) * ((i1 + 1),(j2 + 1))) `2)) / 2 by XREAL_1:74; (((GoB f) * ((i1 + 1),j2)) `2) + (((GoB f) * ((i1 + 1),j2)) `2) < (((GoB f) * ((i1 + 1),j2)) `2) + (((GoB f) * ((i1 + 1),(j2 + 1))) `2) by A104, XREAL_1:8; then A106: ((((GoB f) * ((i1 + 1),j2)) `2) + (((GoB f) * ((i1 + 1),j2)) `2)) / 2 < ((((GoB f) * ((i1 + 1),j2)) `2) + (((GoB f) * ((i1 + 1),(j2 + 1))) `2)) / 2 by XREAL_1:74; p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i1 + 1),j2)) `2 <= s & s <= ((GoB f) * ((i1 + 1),(j2 + 1))) `2 ) } proof p = |[(p `1),(p `2)]| by EUCLID:53; hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i1 + 1),j2)) `2 <= s & s <= ((GoB f) * ((i1 + 1),(j2 + 1))) `2 ) } by A90, A106, A105; ::_thesis: verum end; then A107: p in h_strip ((GoB f),j2) by A3, A8, A99, A86, A98, GOBOARD5:5; A108: ( i1 = 0 or i1 >= 0 + 1 ) by NAT_1:13; A109: now__::_thesis:_(_(_i1_>=_1_&_i1_+_1_<_len_(GoB_f)_&_p_in_(cell_((GoB_f),(i1_+_1),j2))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i1,j2))_/\_((L~_f)_`)_)_or_(_i1_>=_1_&_i1_+_1_=_len_(GoB_f)_&_p_in_(cell_((GoB_f),(i1_+_1),j2))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i1,j2))_/\_((L~_f)_`)_)_or_(_i1_=_0_&_i1_+_1_<_len_(GoB_f)_&_p_in_(cell_((GoB_f),(i1_+_1),j2))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i1,j2))_/\_((L~_f)_`)_)_or_(_i1_=_0_&_i1_+_1_=_len_(GoB_f)_&_contradiction_)_) percases ( ( i1 >= 1 & i1 + 1 < len (GoB f) ) or ( i1 >= 1 & i1 + 1 = len (GoB f) ) or ( i1 = 0 & i1 + 1 < len (GoB f) ) or ( i1 = 0 & i1 + 1 = len (GoB f) ) ) by A3, A8, A108, XXREAL_0:1; caseA110: ( i1 >= 1 & i1 + 1 < len (GoB f) ) ; ::_thesis: ( p in (cell ((GoB f),(i1 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i1,j2)) /\ ((L~ f) `) ) then A111: (i1 + 1) + 1 <= len (GoB f) by NAT_1:13; A112: p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i1 + 1),1)) `1 <= r & r <= ((GoB f) * (((i1 + 1) + 1),1)) `1 ) } proof i1 + 1 < (i1 + 1) + 1 by NAT_1:13; then A113: ((GoB f) * ((i1 + 1),1)) `1 < ((GoB f) * (((i1 + 1) + 1),1)) `1 by A91, A102, A111, GOBOARD5:3; ( ((GoB f) * ((i1 + 1),j2)) `1 = ((GoB f) * ((i1 + 1),1)) `1 & ((GoB f) * ((i1 + 1),(j2 + 1))) `1 = ((GoB f) * ((i1 + 1),1)) `1 ) by A3, A4, A8, A99, A87, A102, A100, GOBOARD5:2; hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i1 + 1),1)) `1 <= r & r <= ((GoB f) * (((i1 + 1) + 1),1)) `1 ) } by A103, A113; ::_thesis: verum end; 1 <= i1 + 1 by NAT_1:11; then p in v_strip ((GoB f),(i1 + 1)) by A91, A110, A112, GOBOARD5:8; then p in (v_strip ((GoB f),(i1 + 1))) /\ (h_strip ((GoB f),j2)) by A107, XBOOLE_0:def_4; then A114: p in cell ((GoB f),(i1 + 1),j2) by GOBOARD5:def_3; A115: p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i1,1)) `1 <= r & r <= ((GoB f) * ((i1 + 1),1)) `1 ) } proof i1 < i1 + 1 by NAT_1:13; then A116: ((GoB f) * (i1,1)) `1 < ((GoB f) * ((i1 + 1),1)) `1 by A91, A110, GOBOARD5:3; ( ((GoB f) * ((i1 + 1),j2)) `1 = ((GoB f) * ((i1 + 1),1)) `1 & ((GoB f) * ((i1 + 1),(j2 + 1))) `1 = ((GoB f) * ((i1 + 1),1)) `1 ) by A3, A4, A8, A99, A87, A102, A100, GOBOARD5:2; hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i1,1)) `1 <= r & r <= ((GoB f) * ((i1 + 1),1)) `1 ) } by A103, A116; ::_thesis: verum end; i1 < len (GoB f) by A110, NAT_1:13; then p in v_strip ((GoB f),i1) by A91, A110, A115, GOBOARD5:8; then p in (v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j2)) by A107, XBOOLE_0:def_4; then p in cell ((GoB f),i1,j2) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),(i1 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i1,j2)) /\ ((L~ f) `) ) by A101, A114, XBOOLE_0:def_4; ::_thesis: verum end; caseA117: ( i1 >= 1 & i1 + 1 = len (GoB f) ) ; ::_thesis: ( p in (cell ((GoB f),(i1 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i1,j2)) /\ ((L~ f) `) ) A118: i1 < i1 + 1 by NAT_1:13; p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i1,1)) `1 <= r & r <= ((GoB f) * ((i1 + 1),1)) `1 ) } proof A119: ((GoB f) * (i1,1)) `1 < ((GoB f) * ((i1 + 1),1)) `1 by A91, A117, A118, GOBOARD5:3; ( ((GoB f) * ((i1 + 1),j2)) `1 = ((GoB f) * ((i1 + 1),1)) `1 & ((GoB f) * ((i1 + 1),(j2 + 1))) `1 = ((GoB f) * ((i1 + 1),1)) `1 ) by A3, A4, A8, A99, A87, A102, A100, GOBOARD5:2; hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i1,1)) `1 <= r & r <= ((GoB f) * ((i1 + 1),1)) `1 ) } by A103, A119; ::_thesis: verum end; then p in v_strip ((GoB f),i1) by A91, A117, A118, GOBOARD5:8; then p in (v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j2)) by A107, XBOOLE_0:def_4; then A120: p in cell ((GoB f),i1,j2) by GOBOARD5:def_3; p in { |[r,s]| where r, s is Real : ((GoB f) * ((i1 + 1),1)) `1 <= r } proof ( ((GoB f) * ((i1 + 1),j2)) `1 = ((GoB f) * ((i1 + 1),1)) `1 & ((GoB f) * ((i1 + 1),(j2 + 1))) `1 = ((GoB f) * ((i1 + 1),1)) `1 ) by A3, A4, A8, A99, A87, A102, A100, GOBOARD5:2; hence p in { |[r,s]| where r, s is Real : ((GoB f) * ((i1 + 1),1)) `1 <= r } by A103; ::_thesis: verum end; then p in v_strip ((GoB f),(i1 + 1)) by A91, A117, GOBOARD5:9; then p in (v_strip ((GoB f),(i1 + 1))) /\ (h_strip ((GoB f),j2)) by A107, XBOOLE_0:def_4; then p in cell ((GoB f),(i1 + 1),j2) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),(i1 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i1,j2)) /\ ((L~ f) `) ) by A101, A120, XBOOLE_0:def_4; ::_thesis: verum end; caseA121: ( i1 = 0 & i1 + 1 < len (GoB f) ) ; ::_thesis: ( p in (cell ((GoB f),(i1 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i1,j2)) /\ ((L~ f) `) ) then A122: (i1 + 1) + 1 <= len (GoB f) by NAT_1:13; p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i1 + 1),1)) `1 <= r & r <= ((GoB f) * (((i1 + 1) + 1),1)) `1 ) } proof i1 + 1 < (i1 + 1) + 1 by NAT_1:13; then A123: ((GoB f) * ((i1 + 1),1)) `1 < ((GoB f) * (((i1 + 1) + 1),1)) `1 by A91, A102, A122, GOBOARD5:3; ( ((GoB f) * ((i1 + 1),j2)) `1 = ((GoB f) * ((i1 + 1),1)) `1 & ((GoB f) * ((i1 + 1),(j2 + 1))) `1 = ((GoB f) * ((i1 + 1),1)) `1 ) by A3, A4, A8, A99, A87, A102, A100, GOBOARD5:2; hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i1 + 1),1)) `1 <= r & r <= ((GoB f) * (((i1 + 1) + 1),1)) `1 ) } by A103, A123; ::_thesis: verum end; then p in v_strip ((GoB f),(i1 + 1)) by A91, A121, GOBOARD5:8; then p in (v_strip ((GoB f),(i1 + 1))) /\ (h_strip ((GoB f),j2)) by A107, XBOOLE_0:def_4; then A124: p in cell ((GoB f),(i1 + 1),j2) by GOBOARD5:def_3; p in { |[r,s]| where r, s is Real : r <= ((GoB f) * (1,1)) `1 } proof ( ((GoB f) * ((i1 + 1),j2)) `1 = ((GoB f) * ((i1 + 1),1)) `1 & ((GoB f) * ((i1 + 1),(j2 + 1))) `1 = ((GoB f) * ((i1 + 1),1)) `1 ) by A3, A4, A8, A99, A87, A102, A100, GOBOARD5:2; hence p in { |[r,s]| where r, s is Real : r <= ((GoB f) * (1,1)) `1 } by A103, A121; ::_thesis: verum end; then p in v_strip ((GoB f),i1) by A91, A121, GOBOARD5:10; then p in (v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j2)) by A107, XBOOLE_0:def_4; then p in cell ((GoB f),i1,j2) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),(i1 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i1,j2)) /\ ((L~ f) `) ) by A101, A124, XBOOLE_0:def_4; ::_thesis: verum end; case ( i1 = 0 & i1 + 1 = len (GoB f) ) ; ::_thesis: contradiction hence contradiction by GOBOARD7:32; ::_thesis: verum end; end; end; then p in Cl (Down ((Int (cell ((GoB f),(i1 + 1),j2))),((L~ f) `))) by A4, Th2; then A125: Cl (Down ((Int (cell ((GoB f),(i1 + 1),j2))),((L~ f) `))) c= Component_of p1 by A3, A4, A8, Th3, GOBRD11:1; p in Cl (Down ((Int (cell ((GoB f),i1,j2))),((L~ f) `))) by A1, A4, A109, Th2; then Component_of p1 c= (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A96, A94, Th5, CONNSP_3:21; then Cl (Down ((Int (cell ((GoB f),(i1 + 1),j2))),((L~ f) `))) c= (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A125, XBOOLE_1:1; hence Int (cell ((GoB f),(i1 + 1),j2)) c= (LeftComp f) \/ (RightComp f) by A95, A97, XBOOLE_1:1; ::_thesis: verum end; end; end; hence Int (cell ((GoB f),(i1 + 1),j2)) c= (LeftComp f) \/ (RightComp f) ; ::_thesis: verum end; end; end; hence Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) by A8; ::_thesis: verum end; caseA126: i1 = i2 + 1 ; ::_thesis: Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) then i2 < i1 by NAT_1:13; then A127: i1 -' 1 < i1 by A126, NAT_D:34; A128: i2 < i2 + 1 by NAT_1:13; A129: 1 <= (i1 -' 1) + 1 by NAT_1:11; A130: i2 + 1 < (i2 + 1) + 1 by NAT_1:13; A131: ( 1 <= i1 & i1 -' 1 = i1 - 1 ) by A126, NAT_1:11, XREAL_0:def_2; A132: 1 <= i2 + 1 by NAT_1:11; A133: i1 -' 1 = i2 by A126, NAT_D:34; now__::_thesis:_(_(_ex_k_being_Element_of_NAT_st_ (_1_<=_k_&_k_+_1_<=_len_f_&_j2_<>_0_&_j2_<>_width_(GoB_f)_&_LSeg_((f_/._k),(f_/._(k_+_1)))_=_LSeg_(((GoB_f)_*_((i2_+_1),j2)),((GoB_f)_*_((i2_+_1),(j2_+_1))))_)_&_Int_(cell_((GoB_f),i2,j2))_c=_(LeftComp_f)_\/_(RightComp_f)_)_or_(_(_for_k_being_Element_of_NAT_holds_ (_not_1_<=_k_or_not_k_+_1_<=_len_f_or_not_j2_<>_0_or_not_j2_<>_width_(GoB_f)_or_not_LSeg_((f_/._k),(f_/._(k_+_1)))_=_LSeg_(((GoB_f)_*_((i2_+_1),j2)),((GoB_f)_*_((i2_+_1),(j2_+_1))))_)_)_&_Int_(cell_((GoB_f),i2,j2))_c=_(LeftComp_f)_\/_(RightComp_f)_)_) percases ( ex k being Element of NAT st ( 1 <= k & k + 1 <= len f & j2 <> 0 & j2 <> width (GoB f) & LSeg ((f /. k),(f /. (k + 1))) = LSeg (((GoB f) * ((i2 + 1),j2)),((GoB f) * ((i2 + 1),(j2 + 1)))) ) or for k being Element of NAT holds ( not 1 <= k or not k + 1 <= len f or not j2 <> 0 or not j2 <> width (GoB f) or not LSeg ((f /. k),(f /. (k + 1))) = LSeg (((GoB f) * ((i2 + 1),j2)),((GoB f) * ((i2 + 1),(j2 + 1)))) ) ) ; case ex k being Element of NAT st ( 1 <= k & k + 1 <= len f & j2 <> 0 & j2 <> width (GoB f) & LSeg ((f /. k),(f /. (k + 1))) = LSeg (((GoB f) * ((i2 + 1),j2)),((GoB f) * ((i2 + 1),(j2 + 1)))) ) ; ::_thesis: Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) then consider k being Element of NAT such that A134: ( 1 <= k & k + 1 <= len f ) and A135: j2 <> 0 and A136: j2 <> width (GoB f) and A137: LSeg ((f /. k),(f /. (k + 1))) = LSeg (((GoB f) * (((i1 -' 1) + 1),j2)),((GoB f) * (((i1 -' 1) + 1),(j2 + 1)))) by A133; now__::_thesis:_(_(_f_/._k_=_(GoB_f)_*_(((i1_-'_1)_+_1),j2)_&_f_/._(k_+_1)_=_(GoB_f)_*_(((i1_-'_1)_+_1),(j2_+_1))_&_Int_(cell_((GoB_f),(i1_-'_1),j2))_c=_(LeftComp_f)_\/_(RightComp_f)_)_or_(_f_/._k_=_(GoB_f)_*_(((i1_-'_1)_+_1),(j2_+_1))_&_f_/._(k_+_1)_=_(GoB_f)_*_(((i1_-'_1)_+_1),j2)_&_Int_(cell_((GoB_f),(i1_-'_1),j2))_c=_(LeftComp_f)_\/_(RightComp_f)_)_) percases ( ( f /. k = (GoB f) * (((i1 -' 1) + 1),j2) & f /. (k + 1) = (GoB f) * (((i1 -' 1) + 1),(j2 + 1)) ) or ( f /. k = (GoB f) * (((i1 -' 1) + 1),(j2 + 1)) & f /. (k + 1) = (GoB f) * (((i1 -' 1) + 1),j2) ) ) by A137, SPPOL_1:8; caseA138: ( f /. k = (GoB f) * (((i1 -' 1) + 1),j2) & f /. (k + 1) = (GoB f) * (((i1 -' 1) + 1),(j2 + 1)) ) ; ::_thesis: Int (cell ((GoB f),(i1 -' 1),j2)) c= (LeftComp f) \/ (RightComp f) A139: ( Int (left_cell (f,k)) c= LeftComp f & LeftComp f c= (LeftComp f) \/ (RightComp f) ) by A134, GOBOARD9:21, XBOOLE_1:7; j2 < width (GoB f) by A4, A136, XXREAL_0:1; then A140: j2 + 1 <= width (GoB f) by NAT_1:13; i1 -' 1 < len (GoB f) by A1, A127, XXREAL_0:2; then (i1 -' 1) + 1 <= len (GoB f) by NAT_1:13; then A141: ( Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] & (i1 -' 1) + 1 in dom (GoB f) ) by A129, FINSEQ_3:25, MATRIX_1:def_4; 1 <= j2 + 1 by NAT_1:11; then j2 + 1 in Seg (width (GoB f)) by A140, FINSEQ_1:1; then A142: [((i1 -' 1) + 1),(j2 + 1)] in Indices (GoB f) by A141, ZFMISC_1:87; j2 >= 0 + 1 by A135, NAT_1:13; then j2 in Seg (width (GoB f)) by A4, FINSEQ_1:1; then [((i1 -' 1) + 1),j2] in Indices (GoB f) by A141, ZFMISC_1:87; then left_cell (f,k) = cell ((GoB f),(i1 -' 1),j2) by A134, A138, A142, GOBOARD5:27; hence Int (cell ((GoB f),(i1 -' 1),j2)) c= (LeftComp f) \/ (RightComp f) by A139, XBOOLE_1:1; ::_thesis: verum end; caseA143: ( f /. k = (GoB f) * (((i1 -' 1) + 1),(j2 + 1)) & f /. (k + 1) = (GoB f) * (((i1 -' 1) + 1),j2) ) ; ::_thesis: Int (cell ((GoB f),(i1 -' 1),j2)) c= (LeftComp f) \/ (RightComp f) A144: ( Int (right_cell (f,k)) c= RightComp f & RightComp f c= (LeftComp f) \/ (RightComp f) ) by A134, GOBOARD9:25, XBOOLE_1:7; j2 < width (GoB f) by A4, A136, XXREAL_0:1; then A145: j2 + 1 <= width (GoB f) by NAT_1:13; A146: ( Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] & (i1 -' 1) + 1 in dom (GoB f) ) by A1, A131, FINSEQ_3:25, MATRIX_1:def_4; 1 <= j2 + 1 by NAT_1:11; then j2 + 1 in Seg (width (GoB f)) by A145, FINSEQ_1:1; then A147: [((i1 -' 1) + 1),(j2 + 1)] in Indices (GoB f) by A146, ZFMISC_1:87; j2 >= 0 + 1 by A135, NAT_1:13; then j2 in Seg (width (GoB f)) by A4, FINSEQ_1:1; then [((i1 -' 1) + 1),j2] in Indices (GoB f) by A146, ZFMISC_1:87; then right_cell (f,k) = cell ((GoB f),(i1 -' 1),j2) by A134, A143, A147, GOBOARD5:30; hence Int (cell ((GoB f),(i1 -' 1),j2)) c= (LeftComp f) \/ (RightComp f) by A144, XBOOLE_1:1; ::_thesis: verum end; end; end; hence Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) by A126, NAT_D:34; ::_thesis: verum end; caseA148: for k being Element of NAT holds ( not 1 <= k or not k + 1 <= len f or not j2 <> 0 or not j2 <> width (GoB f) or not LSeg ((f /. k),(f /. (k + 1))) = LSeg (((GoB f) * ((i2 + 1),j2)),((GoB f) * ((i2 + 1),(j2 + 1)))) ) ; ::_thesis: Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) now__::_thesis:_(_(_j2_=_0_&_Int_(cell_((GoB_f),i2,j2))_c=_(LeftComp_f)_\/_(RightComp_f)_)_or_(_j2_=_width_(GoB_f)_&_Int_(cell_((GoB_f),i2,j2))_c=_(LeftComp_f)_\/_(RightComp_f)_)_or_(_j2_<>_0_&_j2_<>_width_(GoB_f)_&_(_for_k_being_Element_of_NAT_holds_ (_not_1_<=_k_or_not_k_+_1_<=_len_f_or_not_LSeg_((f_/._k),(f_/._(k_+_1)))_=_LSeg_(((GoB_f)_*_((i2_+_1),j2)),((GoB_f)_*_((i2_+_1),(j2_+_1))))_)_)_&_Int_(cell_((GoB_f),i2,j2))_c=_(LeftComp_f)_\/_(RightComp_f)_)_) percases ( j2 = 0 or j2 = width (GoB f) or ( j2 <> 0 & j2 <> width (GoB f) & ( for k being Element of NAT holds ( not 1 <= k or not k + 1 <= len f or not LSeg ((f /. k),(f /. (k + 1))) = LSeg (((GoB f) * ((i2 + 1),j2)),((GoB f) * ((i2 + 1),(j2 + 1)))) ) ) ) ) by A148; caseA149: j2 = 0 ; ::_thesis: Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) reconsider p = |[(((GoB f) * ((i2 + 1),1)) `1),((((GoB f) * ((i2 + 1),1)) `2) - 1)]| as Point of (TOP-REAL 2) ; A150: 1 < width (GoB f) by GOBOARD7:33; A151: 1 < len (GoB f) by GOBOARD7:32; reconsider P = {p} as Subset of (TOP-REAL 2) ; A152: p `2 < (p `2) + 1 by XREAL_1:29; A153: 1 <= i2 + 1 by NAT_1:11; then ((GoB f) * ((i2 + 1),1)) `2 = ((GoB f) * (1,1)) `2 by A1, A126, A150, GOBOARD5:1; then A154: p `2 = (((GoB f) * (1,1)) `2) - 1 by EUCLID:52; p in { |[r,s]| where r, s is Real : s <= ((GoB f) * (1,1)) `2 } proof p = |[(p `1),(p `2)]| by EUCLID:53; hence p in { |[r,s]| where r, s is Real : s <= ((GoB f) * (1,1)) `2 } by A154, A152; ::_thesis: verum end; then A155: p in h_strip ((GoB f),j2) by A149, A151, GOBOARD5:7; ( ( for q being Point of (TOP-REAL 2) st q in P holds q `2 < ((GoB f) * (1,1)) `2 ) implies P misses L~ f ) by GOBOARD8:23; then A156: ( p in {p} & {p} c= (L~ f) ` ) by A154, A152, SUBSET_1:23, TARSKI:def_1; then reconsider p1 = p as Point of ((TOP-REAL 2) | ((L~ f) `)) by PRE_TOPC:8; A157: now__::_thesis:_(_(_i2_+_1_<_len_(GoB_f)_&_i2_>_0_&_p_in_(cell_((GoB_f),(i2_+_1),j2))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i2,j2))_/\_((L~_f)_`)_)_or_(_i2_+_1_<_len_(GoB_f)_&_i2_=_0_&_p_in_(cell_((GoB_f),(i2_+_1),j2))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i2,j2))_/\_((L~_f)_`)_)_or_(_i2_+_1_=_len_(GoB_f)_&_i2_>_0_&_p_in_(cell_((GoB_f),(i2_+_1),j2))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i2,j2))_/\_((L~_f)_`)_)_or_(_i2_+_1_=_len_(GoB_f)_&_i2_=_0_&_p_in_(cell_((GoB_f),(i2_+_1),j2))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i2,j2))_/\_((L~_f)_`)_)_) percases ( ( i2 + 1 < len (GoB f) & i2 > 0 ) or ( i2 + 1 < len (GoB f) & i2 = 0 ) or ( i2 + 1 = len (GoB f) & i2 > 0 ) or ( i2 + 1 = len (GoB f) & i2 = 0 ) ) by A1, A126, XXREAL_0:1; caseA158: ( i2 + 1 < len (GoB f) & i2 > 0 ) ; ::_thesis: ( p in (cell ((GoB f),(i2 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) then A159: (i2 + 1) + 1 <= len (GoB f) by NAT_1:13; A160: p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i2 + 1),1)) `1 <= r & r <= ((GoB f) * (((i2 + 1) + 1),1)) `1 ) } proof i2 + 1 < (i2 + 1) + 1 by NAT_1:13; then ((GoB f) * ((i2 + 1),1)) `1 <= ((GoB f) * (((i2 + 1) + 1),1)) `1 by A150, A153, A159, GOBOARD5:3; hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i2 + 1),1)) `1 <= r & r <= ((GoB f) * (((i2 + 1) + 1),1)) `1 ) } ; ::_thesis: verum end; A161: 0 + 1 <= i2 by A158, NAT_1:13; A162: p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i2,1)) `1 <= r & r <= ((GoB f) * ((i2 + 1),1)) `1 ) } proof i2 < i2 + 1 by NAT_1:13; then ((GoB f) * (i2,1)) `1 < ((GoB f) * ((i2 + 1),1)) `1 by A1, A126, A150, A161, GOBOARD5:3; hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i2,1)) `1 <= r & r <= ((GoB f) * ((i2 + 1),1)) `1 ) } ; ::_thesis: verum end; i2 < len (GoB f) by A158, NAT_1:13; then p in v_strip ((GoB f),i2) by A150, A161, A162, GOBOARD5:8; then p in (v_strip ((GoB f),i2)) /\ (h_strip ((GoB f),j2)) by A155, XBOOLE_0:def_4; then A163: p in cell ((GoB f),i2,j2) by GOBOARD5:def_3; 1 <= i2 + 1 by A161, NAT_1:13; then p in v_strip ((GoB f),(i2 + 1)) by A150, A158, A160, GOBOARD5:8; then p in (v_strip ((GoB f),(i2 + 1))) /\ (h_strip ((GoB f),j2)) by A155, XBOOLE_0:def_4; then p in cell ((GoB f),(i2 + 1),j2) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),(i2 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) by A156, A163, XBOOLE_0:def_4; ::_thesis: verum end; caseA164: ( i2 + 1 < len (GoB f) & i2 = 0 ) ; ::_thesis: ( p in (cell ((GoB f),(i2 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) A165: i2 + 1 < (i2 + 1) + 1 by NAT_1:13; A166: (i2 + 1) + 1 <= len (GoB f) by A164, NAT_1:13; p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i2 + 1),1)) `1 <= r & r <= ((GoB f) * (((i2 + 1) + 1),1)) `1 ) } proof ((GoB f) * ((i2 + 1),1)) `1 < ((GoB f) * (((i2 + 1) + 1),1)) `1 by A132, A150, A166, A165, GOBOARD5:3; hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i2 + 1),1)) `1 <= r & r <= ((GoB f) * (((i2 + 1) + 1),1)) `1 ) } ; ::_thesis: verum end; then p in v_strip ((GoB f),(i2 + 1)) by A150, A164, GOBOARD5:8; then p in (v_strip ((GoB f),(i2 + 1))) /\ (h_strip ((GoB f),j2)) by A155, XBOOLE_0:def_4; then A167: p in cell ((GoB f),(i2 + 1),j2) by GOBOARD5:def_3; p in { |[r,s]| where r, s is Real : r <= ((GoB f) * ((i2 + 1),1)) `1 } ; then p in v_strip ((GoB f),i2) by A150, A164, GOBOARD5:10; then p in (v_strip ((GoB f),i2)) /\ (h_strip ((GoB f),j2)) by A155, XBOOLE_0:def_4; then p in cell ((GoB f),i2,j2) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),(i2 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) by A156, A167, XBOOLE_0:def_4; ::_thesis: verum end; caseA168: ( i2 + 1 = len (GoB f) & i2 > 0 ) ; ::_thesis: ( p in (cell ((GoB f),(i2 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) then A169: 0 + 1 <= i2 by NAT_1:13; A170: p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i2,1)) `1 <= r & r <= ((GoB f) * ((i2 + 1),1)) `1 ) } proof ((GoB f) * (i2,1)) `1 < ((GoB f) * ((i2 + 1),1)) `1 by A128, A150, A168, A169, GOBOARD5:3; hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i2,1)) `1 <= r & r <= ((GoB f) * ((i2 + 1),1)) `1 ) } ; ::_thesis: verum end; p in { |[r,s]| where r, s is Real : ((GoB f) * ((i2 + 1),1)) `1 <= r } ; then p in v_strip ((GoB f),(i2 + 1)) by A150, A168, GOBOARD5:9; then p in (v_strip ((GoB f),(i2 + 1))) /\ (h_strip ((GoB f),j2)) by A155, XBOOLE_0:def_4; then A171: p in cell ((GoB f),(i2 + 1),j2) by GOBOARD5:def_3; i2 < len (GoB f) by A168, NAT_1:13; then p in v_strip ((GoB f),i2) by A150, A169, A170, GOBOARD5:8; then p in (v_strip ((GoB f),i2)) /\ (h_strip ((GoB f),j2)) by A155, XBOOLE_0:def_4; then p in cell ((GoB f),i2,j2) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),(i2 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) by A156, A171, XBOOLE_0:def_4; ::_thesis: verum end; caseA172: ( i2 + 1 = len (GoB f) & i2 = 0 ) ; ::_thesis: ( p in (cell ((GoB f),(i2 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) p in { |[r,s]| where r, s is Real : ((GoB f) * ((i2 + 1),1)) `1 <= r } ; then p in v_strip ((GoB f),(i2 + 1)) by A150, A172, GOBOARD5:9; then p in (v_strip ((GoB f),(i2 + 1))) /\ (h_strip ((GoB f),j2)) by A155, XBOOLE_0:def_4; then A173: p in cell ((GoB f),(i2 + 1),j2) by GOBOARD5:def_3; p in { |[r,s]| where r, s is Real : r <= ((GoB f) * (1,1)) `1 } by A172; then p in v_strip ((GoB f),i2) by A150, A172, GOBOARD5:10; then p in (v_strip ((GoB f),i2)) /\ (h_strip ((GoB f),j2)) by A155, XBOOLE_0:def_4; then p in cell ((GoB f),i2,j2) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),(i2 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) by A156, A173, XBOOLE_0:def_4; ::_thesis: verum end; end; end; then p in Cl (Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `))) by A3, A4, Th2; then A174: Cl (Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `))) c= Component_of p1 by A3, A4, Th3, GOBRD11:1; Down ((RightComp f),((L~ f) `)) is closed by Lm4, CONNSP_1:33; then A175: Cl (Down ((RightComp f),((L~ f) `))) = Down ((RightComp f),((L~ f) `)) by PRE_TOPC:22; Down ((LeftComp f),((L~ f) `)) is closed by Lm3, CONNSP_1:33; then A176: Cl (Down ((LeftComp f),((L~ f) `))) = Down ((LeftComp f),((L~ f) `)) by PRE_TOPC:22; A177: ( Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `)) c= Cl (Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `))) & Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `)) = Int (cell ((GoB f),i2,j2)) ) by A3, A4, Th3, PRE_TOPC:18; (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) = Down (((LeftComp f) \/ (RightComp f)),((L~ f) `)) by GOBRD11:4; then A178: Cl (Down (((LeftComp f) \/ (RightComp f)),((L~ f) `))) = (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A176, A175, PRE_TOPC:20; A179: ( Down ((LeftComp f),((L~ f) `)) = LeftComp f & Down ((RightComp f),((L~ f) `)) = RightComp f ) by Th5; Down ((Int (cell ((GoB f),i1,j2))),((L~ f) `)) c= (LeftComp f) \/ (RightComp f) by A1, A2, A6, A7, Th3; then Down ((Int (cell ((GoB f),i1,j2))),((L~ f) `)) c= Down (((LeftComp f) \/ (RightComp f)),((L~ f) `)) by A179, GOBRD11:4; then A180: Cl (Down ((Int (cell ((GoB f),i1,j2))),((L~ f) `))) c= Cl (Down (((LeftComp f) \/ (RightComp f)),((L~ f) `))) by PRE_TOPC:19; p in Cl (Down ((Int (cell ((GoB f),(i2 + 1),j2))),((L~ f) `))) by A4, A157, Th2; then Component_of p1 c= (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A126, A180, A178, Th5, CONNSP_3:21; then Cl (Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `))) c= (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A174, XBOOLE_1:1; hence Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) by A179, A177, XBOOLE_1:1; ::_thesis: verum end; caseA181: j2 = width (GoB f) ; ::_thesis: Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) reconsider p = |[(((GoB f) * ((i2 + 1),(width (GoB f)))) `1),((((GoB f) * ((i2 + 1),(width (GoB f)))) `2) + 1)]| as Point of (TOP-REAL 2) ; A182: 1 < width (GoB f) by GOBOARD7:33; reconsider P = {p} as Subset of (TOP-REAL 2) ; A183: ( ( for q being Point of (TOP-REAL 2) st q in P holds ((GoB f) * (1,(width (GoB f)))) `2 < q `2 ) implies P misses L~ f ) by GOBOARD8:24; A184: 1 < len (GoB f) by GOBOARD7:32; A185: 1 <= i2 + 1 by NAT_1:11; then ((GoB f) * ((i2 + 1),(width (GoB f)))) `2 = ((GoB f) * (1,(width (GoB f)))) `2 by A1, A126, A182, GOBOARD5:1; then A186: p `2 = (((GoB f) * (1,(width (GoB f)))) `2) + 1 by EUCLID:52; p in { |[r,s]| where r, s is Real : ((GoB f) * (1,(width (GoB f)))) `2 <= s } proof ( p = |[(p `1),(p `2)]| & ((GoB f) * (1,(width (GoB f)))) `2 <= p `2 ) by A186, EUCLID:53, XREAL_1:29; hence p in { |[r,s]| where r, s is Real : ((GoB f) * (1,(width (GoB f)))) `2 <= s } ; ::_thesis: verum end; then A187: p in h_strip ((GoB f),j2) by A181, A184, GOBOARD5:6; ((GoB f) * (1,(width (GoB f)))) `2 < (((GoB f) * (1,(width (GoB f)))) `2) + 1 by XREAL_1:29; then A188: ( p in {p} & {p} c= (L~ f) ` ) by A186, A183, SUBSET_1:23, TARSKI:def_1; then reconsider p1 = p as Point of ((TOP-REAL 2) | ((L~ f) `)) by PRE_TOPC:8; A189: now__::_thesis:_(_(_i2_+_1_<_len_(GoB_f)_&_i2_>_0_&_p_in_(cell_((GoB_f),(i2_+_1),j2))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i2,j2))_/\_((L~_f)_`)_)_or_(_i2_+_1_<_len_(GoB_f)_&_i2_=_0_&_p_in_(cell_((GoB_f),(i2_+_1),j2))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i2,j2))_/\_((L~_f)_`)_)_or_(_i2_+_1_=_len_(GoB_f)_&_i2_>_0_&_p_in_(cell_((GoB_f),(i2_+_1),j2))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i2,j2))_/\_((L~_f)_`)_)_or_(_i2_+_1_=_len_(GoB_f)_&_i2_=_0_&_contradiction_)_) percases ( ( i2 + 1 < len (GoB f) & i2 > 0 ) or ( i2 + 1 < len (GoB f) & i2 = 0 ) or ( i2 + 1 = len (GoB f) & i2 > 0 ) or ( i2 + 1 = len (GoB f) & i2 = 0 ) ) by A1, A126, XXREAL_0:1; caseA190: ( i2 + 1 < len (GoB f) & i2 > 0 ) ; ::_thesis: ( p in (cell ((GoB f),(i2 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) then A191: (i2 + 1) + 1 <= len (GoB f) by NAT_1:13; A192: p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i2 + 1),(width (GoB f)))) `1 <= r & r <= ((GoB f) * (((i2 + 1) + 1),(width (GoB f)))) `1 ) } proof i2 + 1 < (i2 + 1) + 1 by NAT_1:13; then ((GoB f) * ((i2 + 1),(width (GoB f)))) `1 <= ((GoB f) * (((i2 + 1) + 1),(width (GoB f)))) `1 by A182, A185, A191, GOBOARD5:3; hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i2 + 1),(width (GoB f)))) `1 <= r & r <= ((GoB f) * (((i2 + 1) + 1),(width (GoB f)))) `1 ) } ; ::_thesis: verum end; 1 <= i2 + 1 by NAT_1:11; then p in v_strip ((GoB f),(i2 + 1)) by A182, A190, A192, GOBOARD5:8; then p in (v_strip ((GoB f),(i2 + 1))) /\ (h_strip ((GoB f),j2)) by A187, XBOOLE_0:def_4; then A193: p in cell ((GoB f),(i2 + 1),j2) by GOBOARD5:def_3; A194: 0 + 1 <= i2 by A190, NAT_1:13; A195: i2 < i2 + 1 by NAT_1:13; A196: p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i2,(width (GoB f)))) `1 <= r & r <= ((GoB f) * ((i2 + 1),(width (GoB f)))) `1 ) } proof ((GoB f) * (i2,(width (GoB f)))) `1 < ((GoB f) * ((i2 + 1),(width (GoB f)))) `1 by A1, A126, A182, A194, A195, GOBOARD5:3; hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i2,(width (GoB f)))) `1 <= r & r <= ((GoB f) * ((i2 + 1),(width (GoB f)))) `1 ) } ; ::_thesis: verum end; i2 < len (GoB f) by A190, NAT_1:13; then p in v_strip ((GoB f),i2) by A182, A194, A196, GOBOARD5:8; then p in (v_strip ((GoB f),i2)) /\ (h_strip ((GoB f),j2)) by A187, XBOOLE_0:def_4; then p in cell ((GoB f),i2,j2) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),(i2 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) by A188, A193, XBOOLE_0:def_4; ::_thesis: verum end; caseA197: ( i2 + 1 < len (GoB f) & i2 = 0 ) ; ::_thesis: ( p in (cell ((GoB f),(i2 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) then A198: (i2 + 1) + 1 <= len (GoB f) by NAT_1:13; p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i2 + 1),(width (GoB f)))) `1 <= r & r <= ((GoB f) * (((i2 + 1) + 1),(width (GoB f)))) `1 ) } proof ((GoB f) * ((i2 + 1),(width (GoB f)))) `1 < ((GoB f) * (((i2 + 1) + 1),(width (GoB f)))) `1 by A132, A130, A182, A198, GOBOARD5:3; hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i2 + 1),(width (GoB f)))) `1 <= r & r <= ((GoB f) * (((i2 + 1) + 1),(width (GoB f)))) `1 ) } ; ::_thesis: verum end; then p in v_strip ((GoB f),(i2 + 1)) by A182, A197, GOBOARD5:8; then p in (v_strip ((GoB f),(i2 + 1))) /\ (h_strip ((GoB f),j2)) by A187, XBOOLE_0:def_4; then A199: p in cell ((GoB f),(i2 + 1),j2) by GOBOARD5:def_3; p in { |[r,s]| where r, s is Real : r <= ((GoB f) * (1,(width (GoB f)))) `1 } by A197; then p in v_strip ((GoB f),i2) by A182, A197, GOBOARD5:10; then p in (v_strip ((GoB f),i2)) /\ (h_strip ((GoB f),j2)) by A187, XBOOLE_0:def_4; then p in cell ((GoB f),i2,j2) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),(i2 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) by A188, A199, XBOOLE_0:def_4; ::_thesis: verum end; caseA200: ( i2 + 1 = len (GoB f) & i2 > 0 ) ; ::_thesis: ( p in (cell ((GoB f),(i2 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) then A201: 0 + 1 <= i2 by NAT_1:13; A202: p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i2,(width (GoB f)))) `1 <= r & r <= ((GoB f) * ((i2 + 1),(width (GoB f)))) `1 ) } proof ((GoB f) * (i2,(width (GoB f)))) `1 <= ((GoB f) * ((i2 + 1),(width (GoB f)))) `1 by A128, A182, A200, A201, GOBOARD5:3; hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i2,(width (GoB f)))) `1 <= r & r <= ((GoB f) * ((i2 + 1),(width (GoB f)))) `1 ) } ; ::_thesis: verum end; p in { |[r,s]| where r, s is Real : ((GoB f) * ((len (GoB f)),(width (GoB f)))) `1 <= r } by A200; then p in v_strip ((GoB f),(i2 + 1)) by A182, A200, GOBOARD5:9; then p in (v_strip ((GoB f),(i2 + 1))) /\ (h_strip ((GoB f),j2)) by A187, XBOOLE_0:def_4; then A203: p in cell ((GoB f),(i2 + 1),j2) by GOBOARD5:def_3; i2 < len (GoB f) by A200, NAT_1:13; then p in v_strip ((GoB f),i2) by A182, A201, A202, GOBOARD5:8; then p in (v_strip ((GoB f),i2)) /\ (h_strip ((GoB f),j2)) by A187, XBOOLE_0:def_4; then p in cell ((GoB f),i2,j2) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),(i2 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) by A188, A203, XBOOLE_0:def_4; ::_thesis: verum end; case ( i2 + 1 = len (GoB f) & i2 = 0 ) ; ::_thesis: contradiction hence contradiction by GOBOARD7:32; ::_thesis: verum end; end; end; then p in Cl (Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `))) by A3, A4, Th2; then A204: Cl (Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `))) c= Component_of p1 by A3, A4, Th3, GOBRD11:1; Down ((RightComp f),((L~ f) `)) is closed by Lm4, CONNSP_1:33; then A205: Cl (Down ((RightComp f),((L~ f) `))) = Down ((RightComp f),((L~ f) `)) by PRE_TOPC:22; Down ((LeftComp f),((L~ f) `)) is closed by Lm3, CONNSP_1:33; then A206: Cl (Down ((LeftComp f),((L~ f) `))) = Down ((LeftComp f),((L~ f) `)) by PRE_TOPC:22; A207: ( Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `)) c= Cl (Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `))) & Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `)) = Int (cell ((GoB f),i2,j2)) ) by A3, A4, Th3, PRE_TOPC:18; (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) = Down (((LeftComp f) \/ (RightComp f)),((L~ f) `)) by GOBRD11:4; then A208: Cl (Down (((LeftComp f) \/ (RightComp f)),((L~ f) `))) = (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A206, A205, PRE_TOPC:20; A209: ( Down ((LeftComp f),((L~ f) `)) = LeftComp f & Down ((RightComp f),((L~ f) `)) = RightComp f ) by Th5; Down ((Int (cell ((GoB f),i1,j2))),((L~ f) `)) c= (LeftComp f) \/ (RightComp f) by A1, A2, A6, A7, Th3; then Down ((Int (cell ((GoB f),i1,j2))),((L~ f) `)) c= Down (((LeftComp f) \/ (RightComp f)),((L~ f) `)) by A209, GOBRD11:4; then A210: Cl (Down ((Int (cell ((GoB f),i1,j2))),((L~ f) `))) c= Cl (Down (((LeftComp f) \/ (RightComp f)),((L~ f) `))) by PRE_TOPC:19; p in Cl (Down ((Int (cell ((GoB f),(i2 + 1),j2))),((L~ f) `))) by A4, A189, Th2; then Component_of p1 c= (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A126, A210, A208, Th5, CONNSP_3:21; then Cl (Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `))) c= (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A204, XBOOLE_1:1; hence Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) by A209, A207, XBOOLE_1:1; ::_thesis: verum end; caseA211: ( j2 <> 0 & j2 <> width (GoB f) & ( for k being Element of NAT holds ( not 1 <= k or not k + 1 <= len f or not LSeg ((f /. k),(f /. (k + 1))) = LSeg (((GoB f) * ((i2 + 1),j2)),((GoB f) * ((i2 + 1),(j2 + 1)))) ) ) ) ; ::_thesis: Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) then A212: j2 < width (GoB f) by A4, XXREAL_0:1; then A213: j2 + 1 <= width (GoB f) by NAT_1:13; for k being Element of NAT st 1 <= k & k + 1 <= len f holds LSeg (((GoB f) * ((i2 + 1),j2)),((GoB f) * ((i2 + 1),(j2 + 1)))) <> LSeg (f,k) proof let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f implies LSeg (((GoB f) * ((i2 + 1),j2)),((GoB f) * ((i2 + 1),(j2 + 1)))) <> LSeg (f,k) ) assume A214: ( 1 <= k & k + 1 <= len f ) ; ::_thesis: LSeg (((GoB f) * ((i2 + 1),j2)),((GoB f) * ((i2 + 1),(j2 + 1)))) <> LSeg (f,k) then LSeg (f,k) = LSeg ((f /. k),(f /. (k + 1))) by TOPREAL1:def_3; hence LSeg (((GoB f) * ((i2 + 1),j2)),((GoB f) * ((i2 + 1),(j2 + 1)))) <> LSeg (f,k) by A211, A214; ::_thesis: verum end; then A215: ( 1 <= i2 + 1 & i2 + 1 <= len (GoB f) & 1 <= j2 & j2 + 1 <= width (GoB f) implies not (1 / 2) * (((GoB f) * ((i2 + 1),j2)) + ((GoB f) * ((i2 + 1),(j2 + 1)))) in L~ f ) by GOBOARD7:39; reconsider p = (1 / 2) * (((GoB f) * ((i2 + 1),j2)) + ((GoB f) * ((i2 + 1),(j2 + 1)))) as Point of (TOP-REAL 2) ; A216: p `2 = (1 / 2) * ((((GoB f) * ((i2 + 1),j2)) + ((GoB f) * ((i2 + 1),(j2 + 1)))) `2) by TOPREAL3:4 .= (1 / 2) * ((((GoB f) * ((i2 + 1),j2)) `2) + (((GoB f) * ((i2 + 1),(j2 + 1))) `2)) by TOPREAL3:2 ; reconsider P = {p} as Subset of (TOP-REAL 2) ; A217: 1 < width (GoB f) by GOBOARD7:33; Down ((RightComp f),((L~ f) `)) is closed by Lm4, CONNSP_1:33; then A218: Cl (Down ((RightComp f),((L~ f) `))) = Down ((RightComp f),((L~ f) `)) by PRE_TOPC:22; Down ((LeftComp f),((L~ f) `)) is closed by Lm3, CONNSP_1:33; then A219: Cl (Down ((LeftComp f),((L~ f) `))) = Down ((LeftComp f),((L~ f) `)) by PRE_TOPC:22; (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) = Down (((LeftComp f) \/ (RightComp f)),((L~ f) `)) by GOBRD11:4; then A220: Cl (Down (((LeftComp f) \/ (RightComp f)),((L~ f) `))) = (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A219, A218, PRE_TOPC:20; A221: 1 <= i2 + 1 by NAT_1:11; p `1 = (1 / 2) * ((((GoB f) * ((i2 + 1),j2)) + ((GoB f) * ((i2 + 1),(j2 + 1)))) `1) by TOPREAL3:4 .= (1 / 2) * ((((GoB f) * ((i2 + 1),j2)) `1) + (((GoB f) * ((i2 + 1),(j2 + 1))) `1)) by TOPREAL3:2 ; then A222: p = |[((1 / 2) * ((((GoB f) * ((i2 + 1),j2)) `1) + (((GoB f) * ((i2 + 1),(j2 + 1))) `1))),((1 / 2) * ((((GoB f) * ((i2 + 1),j2)) `2) + (((GoB f) * ((i2 + 1),(j2 + 1))) `2)))]| by A216, EUCLID:53; A223: ( Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `)) c= Cl (Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `))) & Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `)) = Int (cell ((GoB f),i2,j2)) ) by A3, A4, Th3, PRE_TOPC:18; A224: ( Down ((LeftComp f),((L~ f) `)) = LeftComp f & Down ((RightComp f),((L~ f) `)) = RightComp f ) by Th5; Down ((Int (cell ((GoB f),i1,j2))),((L~ f) `)) c= (LeftComp f) \/ (RightComp f) by A1, A2, A6, A7, Th3; then Down ((Int (cell ((GoB f),i1,j2))),((L~ f) `)) c= Down (((LeftComp f) \/ (RightComp f)),((L~ f) `)) by A224, GOBRD11:4; then A225: Cl (Down ((Int (cell ((GoB f),i1,j2))),((L~ f) `))) c= Cl (Down (((LeftComp f) \/ (RightComp f)),((L~ f) `))) by PRE_TOPC:19; A226: 0 + 1 <= j2 by A211, NAT_1:13; then A227: 1 < j2 + 1 by NAT_1:13; ( ( for x being set st x in P holds not x in L~ f ) implies P misses L~ f ) by XBOOLE_0:3; then A228: ( p in {p} & {p} c= (L~ f) ` ) by A1, A126, A226, A212, A215, NAT_1:13, SUBSET_1:23, TARSKI:def_1; then reconsider p1 = p as Point of ((TOP-REAL 2) | ((L~ f) `)) by PRE_TOPC:8; A229: 1 <= 1 + i2 by NAT_1:11; j2 < j2 + 1 by NAT_1:13; then A230: ((GoB f) * ((i2 + 1),j2)) `2 < ((GoB f) * ((i2 + 1),(j2 + 1))) `2 by A1, A126, A226, A213, A229, GOBOARD5:4; then (((GoB f) * ((i2 + 1),j2)) `2) + (((GoB f) * ((i2 + 1),(j2 + 1))) `2) < (((GoB f) * ((i2 + 1),(j2 + 1))) `2) + (((GoB f) * ((i2 + 1),(j2 + 1))) `2) by XREAL_1:8; then A231: ((((GoB f) * ((i2 + 1),j2)) `2) + (((GoB f) * ((i2 + 1),(j2 + 1))) `2)) / 2 < ((((GoB f) * ((i2 + 1),(j2 + 1))) `2) + (((GoB f) * ((i2 + 1),(j2 + 1))) `2)) / 2 by XREAL_1:74; (((GoB f) * ((i2 + 1),j2)) `2) + (((GoB f) * ((i2 + 1),j2)) `2) < (((GoB f) * ((i2 + 1),j2)) `2) + (((GoB f) * ((i2 + 1),(j2 + 1))) `2) by A230, XREAL_1:8; then A232: ((((GoB f) * ((i2 + 1),j2)) `2) + (((GoB f) * ((i2 + 1),j2)) `2)) / 2 < ((((GoB f) * ((i2 + 1),j2)) `2) + (((GoB f) * ((i2 + 1),(j2 + 1))) `2)) / 2 by XREAL_1:74; p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i2 + 1),j2)) `2 <= s & s <= ((GoB f) * ((i2 + 1),(j2 + 1))) `2 ) } proof p = |[(p `1),(p `2)]| by EUCLID:53; hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i2 + 1),j2)) `2 <= s & s <= ((GoB f) * ((i2 + 1),(j2 + 1))) `2 ) } by A216, A232, A231; ::_thesis: verum end; then A233: p in h_strip ((GoB f),j2) by A1, A126, A226, A212, A221, GOBOARD5:5; A234: ( i2 = 0 or i2 >= 0 + 1 ) by NAT_1:13; A235: now__::_thesis:_(_(_i2_>=_1_&_i2_+_1_<_len_(GoB_f)_&_p_in_(cell_((GoB_f),(i2_+_1),j2))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i2,j2))_/\_((L~_f)_`)_)_or_(_i2_>=_1_&_i2_+_1_=_len_(GoB_f)_&_p_in_(cell_((GoB_f),(i2_+_1),j2))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i2,j2))_/\_((L~_f)_`)_)_or_(_i2_=_0_&_i2_+_1_<_len_(GoB_f)_&_p_in_(cell_((GoB_f),(i2_+_1),j2))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i2,j2))_/\_((L~_f)_`)_)_or_(_i2_=_0_&_i2_+_1_=_len_(GoB_f)_&_contradiction_)_) percases ( ( i2 >= 1 & i2 + 1 < len (GoB f) ) or ( i2 >= 1 & i2 + 1 = len (GoB f) ) or ( i2 = 0 & i2 + 1 < len (GoB f) ) or ( i2 = 0 & i2 + 1 = len (GoB f) ) ) by A1, A126, A234, XXREAL_0:1; caseA236: ( i2 >= 1 & i2 + 1 < len (GoB f) ) ; ::_thesis: ( p in (cell ((GoB f),(i2 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) then A237: (i2 + 1) + 1 <= len (GoB f) by NAT_1:13; A238: p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i2 + 1),1)) `1 <= r & r <= ((GoB f) * (((i2 + 1) + 1),1)) `1 ) } proof i2 + 1 < (i2 + 1) + 1 by NAT_1:13; then A239: ((GoB f) * ((i2 + 1),1)) `1 < ((GoB f) * (((i2 + 1) + 1),1)) `1 by A217, A229, A237, GOBOARD5:3; ( ((GoB f) * ((i2 + 1),j2)) `1 = ((GoB f) * ((i2 + 1),1)) `1 & ((GoB f) * ((i2 + 1),(j2 + 1))) `1 = ((GoB f) * ((i2 + 1),1)) `1 ) by A1, A4, A126, A226, A213, A229, A227, GOBOARD5:2; hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i2 + 1),1)) `1 <= r & r <= ((GoB f) * (((i2 + 1) + 1),1)) `1 ) } by A222, A239; ::_thesis: verum end; 1 <= i2 + 1 by NAT_1:11; then p in v_strip ((GoB f),(i2 + 1)) by A217, A236, A238, GOBOARD5:8; then p in (v_strip ((GoB f),(i2 + 1))) /\ (h_strip ((GoB f),j2)) by A233, XBOOLE_0:def_4; then A240: p in cell ((GoB f),(i2 + 1),j2) by GOBOARD5:def_3; A241: p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i2,1)) `1 <= r & r <= ((GoB f) * ((i2 + 1),1)) `1 ) } proof i2 < i2 + 1 by NAT_1:13; then A242: ((GoB f) * (i2,1)) `1 < ((GoB f) * ((i2 + 1),1)) `1 by A217, A236, GOBOARD5:3; ( ((GoB f) * ((i2 + 1),j2)) `1 = ((GoB f) * ((i2 + 1),1)) `1 & ((GoB f) * ((i2 + 1),(j2 + 1))) `1 = ((GoB f) * ((i2 + 1),1)) `1 ) by A1, A4, A126, A226, A213, A229, A227, GOBOARD5:2; hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i2,1)) `1 <= r & r <= ((GoB f) * ((i2 + 1),1)) `1 ) } by A222, A242; ::_thesis: verum end; i2 < len (GoB f) by A236, NAT_1:13; then p in v_strip ((GoB f),i2) by A217, A236, A241, GOBOARD5:8; then p in (v_strip ((GoB f),i2)) /\ (h_strip ((GoB f),j2)) by A233, XBOOLE_0:def_4; then p in cell ((GoB f),i2,j2) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),(i2 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) by A228, A240, XBOOLE_0:def_4; ::_thesis: verum end; caseA243: ( i2 >= 1 & i2 + 1 = len (GoB f) ) ; ::_thesis: ( p in (cell ((GoB f),(i2 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) A244: i2 < i2 + 1 by NAT_1:13; p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i2,1)) `1 <= r & r <= ((GoB f) * ((i2 + 1),1)) `1 ) } proof A245: ((GoB f) * (i2,1)) `1 < ((GoB f) * ((i2 + 1),1)) `1 by A217, A243, A244, GOBOARD5:3; ( ((GoB f) * ((i2 + 1),j2)) `1 = ((GoB f) * ((i2 + 1),1)) `1 & ((GoB f) * ((i2 + 1),(j2 + 1))) `1 = ((GoB f) * ((i2 + 1),1)) `1 ) by A1, A4, A126, A226, A213, A229, A227, GOBOARD5:2; hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i2,1)) `1 <= r & r <= ((GoB f) * ((i2 + 1),1)) `1 ) } by A222, A245; ::_thesis: verum end; then p in v_strip ((GoB f),i2) by A217, A243, A244, GOBOARD5:8; then p in (v_strip ((GoB f),i2)) /\ (h_strip ((GoB f),j2)) by A233, XBOOLE_0:def_4; then A246: p in cell ((GoB f),i2,j2) by GOBOARD5:def_3; p in { |[r,s]| where r, s is Real : ((GoB f) * ((i2 + 1),1)) `1 <= r } proof ( ((GoB f) * ((i2 + 1),j2)) `1 = ((GoB f) * ((i2 + 1),1)) `1 & ((GoB f) * ((i2 + 1),(j2 + 1))) `1 = ((GoB f) * ((i2 + 1),1)) `1 ) by A1, A4, A126, A226, A213, A229, A227, GOBOARD5:2; hence p in { |[r,s]| where r, s is Real : ((GoB f) * ((i2 + 1),1)) `1 <= r } by A222; ::_thesis: verum end; then p in v_strip ((GoB f),(i2 + 1)) by A217, A243, GOBOARD5:9; then p in (v_strip ((GoB f),(i2 + 1))) /\ (h_strip ((GoB f),j2)) by A233, XBOOLE_0:def_4; then p in cell ((GoB f),(i2 + 1),j2) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),(i2 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) by A228, A246, XBOOLE_0:def_4; ::_thesis: verum end; caseA247: ( i2 = 0 & i2 + 1 < len (GoB f) ) ; ::_thesis: ( p in (cell ((GoB f),(i2 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) then A248: (i2 + 1) + 1 <= len (GoB f) by NAT_1:13; p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i2 + 1),1)) `1 <= r & r <= ((GoB f) * (((i2 + 1) + 1),1)) `1 ) } proof i2 + 1 < (i2 + 1) + 1 by NAT_1:13; then A249: ((GoB f) * ((i2 + 1),1)) `1 < ((GoB f) * (((i2 + 1) + 1),1)) `1 by A217, A229, A248, GOBOARD5:3; ( ((GoB f) * ((i2 + 1),j2)) `1 = ((GoB f) * ((i2 + 1),1)) `1 & ((GoB f) * ((i2 + 1),(j2 + 1))) `1 = ((GoB f) * ((i2 + 1),1)) `1 ) by A1, A4, A126, A226, A213, A229, A227, GOBOARD5:2; hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i2 + 1),1)) `1 <= r & r <= ((GoB f) * (((i2 + 1) + 1),1)) `1 ) } by A222, A249; ::_thesis: verum end; then p in v_strip ((GoB f),i1) by A126, A217, A247, GOBOARD5:8; then p in (v_strip ((GoB f),(i2 + 1))) /\ (h_strip ((GoB f),j2)) by A126, A233, XBOOLE_0:def_4; then A250: p in cell ((GoB f),(i2 + 1),j2) by GOBOARD5:def_3; p in { |[r,s]| where r, s is Real : r <= ((GoB f) * (1,1)) `1 } proof ( ((GoB f) * ((i2 + 1),j2)) `1 = ((GoB f) * ((i2 + 1),1)) `1 & ((GoB f) * ((i2 + 1),(j2 + 1))) `1 = ((GoB f) * ((i2 + 1),1)) `1 ) by A1, A4, A126, A226, A213, A229, A227, GOBOARD5:2; hence p in { |[r,s]| where r, s is Real : r <= ((GoB f) * (1,1)) `1 } by A222, A247; ::_thesis: verum end; then p in v_strip ((GoB f),i2) by A217, A247, GOBOARD5:10; then p in (v_strip ((GoB f),i2)) /\ (h_strip ((GoB f),j2)) by A233, XBOOLE_0:def_4; then p in cell ((GoB f),i2,j2) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),(i2 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) by A228, A250, XBOOLE_0:def_4; ::_thesis: verum end; case ( i2 = 0 & i2 + 1 = len (GoB f) ) ; ::_thesis: contradiction hence contradiction by GOBOARD7:32; ::_thesis: verum end; end; end; then p in Cl (Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `))) by A3, A4, Th2; then A251: Cl (Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `))) c= Component_of p1 by A3, A4, Th3, GOBRD11:1; p in Cl (Down ((Int (cell ((GoB f),i1,j2))),((L~ f) `))) by A4, A126, A235, Th2; then Component_of p1 c= (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A225, A220, Th5, CONNSP_3:21; then Cl (Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `))) c= (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A251, XBOOLE_1:1; hence Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) by A224, A223, XBOOLE_1:1; ::_thesis: verum end; end; end; hence Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) ; ::_thesis: verum end; end; end; hence Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) ; ::_thesis: verum end; end; end; hence Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) ; ::_thesis: verum end; hence ( not Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) or Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) ) ; ::_thesis: verum end; Lm6: for f being non constant standard special_circular_sequence for i1, j1, i2, j2 being Element of NAT st i1 <= len (GoB f) & j1 <= width (GoB f) & i2 <= len (GoB f) & j2 <= width (GoB f) & ( j2 = j1 + 1 or j1 = j2 + 1 ) & i1 = i2 & Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) holds Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) proof let f be non constant standard special_circular_sequence; ::_thesis: for i1, j1, i2, j2 being Element of NAT st i1 <= len (GoB f) & j1 <= width (GoB f) & i2 <= len (GoB f) & j2 <= width (GoB f) & ( j2 = j1 + 1 or j1 = j2 + 1 ) & i1 = i2 & Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) holds Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) let i1, j1, i2, j2 be Element of NAT ; ::_thesis: ( i1 <= len (GoB f) & j1 <= width (GoB f) & i2 <= len (GoB f) & j2 <= width (GoB f) & ( j2 = j1 + 1 or j1 = j2 + 1 ) & i1 = i2 & Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) implies Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) ) assume that A1: i1 <= len (GoB f) and A2: j1 <= width (GoB f) and A3: i2 <= len (GoB f) and A4: j2 <= width (GoB f) and A5: ( j2 = j1 + 1 or j1 = j2 + 1 ) and A6: i1 = i2 ; ::_thesis: ( not Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) or Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) ) now__::_thesis:_(_Int_(cell_((GoB_f),i1,j1))_c=_(LeftComp_f)_\/_(RightComp_f)_implies_Int_(cell_((GoB_f),i2,j2))_c=_(LeftComp_f)_\/_(RightComp_f)_) assume A7: Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) ; ::_thesis: Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) now__::_thesis:_(_(_j2_=_j1_+_1_&_Int_(cell_((GoB_f),i2,j2))_c=_(LeftComp_f)_\/_(RightComp_f)_)_or_(_j1_=_j2_+_1_&_Int_(cell_((GoB_f),i2,j2))_c=_(LeftComp_f)_\/_(RightComp_f)_)_) percases ( j2 = j1 + 1 or j1 = j2 + 1 ) by A5; caseA8: j2 = j1 + 1 ; ::_thesis: Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) now__::_thesis:_(_(_ex_k_being_Element_of_NAT_st_ (_1_<=_k_&_k_+_1_<=_len_f_&_i2_<>_0_&_i2_<>_len_(GoB_f)_&_LSeg_((f_/._k),(f_/._(k_+_1)))_=_LSeg_(((GoB_f)_*_(i2,(j1_+_1))),((GoB_f)_*_((i2_+_1),(j1_+_1))))_)_&_Int_(cell_((GoB_f),i2,(j1_+_1)))_c=_(LeftComp_f)_\/_(RightComp_f)_)_or_(_(_for_k_being_Element_of_NAT_holds_ (_not_1_<=_k_or_not_k_+_1_<=_len_f_or_not_i2_<>_0_or_not_i2_<>_len_(GoB_f)_or_not_LSeg_((f_/._k),(f_/._(k_+_1)))_=_LSeg_(((GoB_f)_*_(i2,(j1_+_1))),((GoB_f)_*_((i2_+_1),(j1_+_1))))_)_)_&_Int_(cell_((GoB_f),i2,(j1_+_1)))_c=_(LeftComp_f)_\/_(RightComp_f)_)_) percases ( ex k being Element of NAT st ( 1 <= k & k + 1 <= len f & i2 <> 0 & i2 <> len (GoB f) & LSeg ((f /. k),(f /. (k + 1))) = LSeg (((GoB f) * (i2,(j1 + 1))),((GoB f) * ((i2 + 1),(j1 + 1)))) ) or for k being Element of NAT holds ( not 1 <= k or not k + 1 <= len f or not i2 <> 0 or not i2 <> len (GoB f) or not LSeg ((f /. k),(f /. (k + 1))) = LSeg (((GoB f) * (i2,(j1 + 1))),((GoB f) * ((i2 + 1),(j1 + 1)))) ) ) ; case ex k being Element of NAT st ( 1 <= k & k + 1 <= len f & i2 <> 0 & i2 <> len (GoB f) & LSeg ((f /. k),(f /. (k + 1))) = LSeg (((GoB f) * (i2,(j1 + 1))),((GoB f) * ((i2 + 1),(j1 + 1)))) ) ; ::_thesis: Int (cell ((GoB f),i2,(j1 + 1))) c= (LeftComp f) \/ (RightComp f) then consider k being Element of NAT such that A9: ( 1 <= k & k + 1 <= len f ) and A10: i2 <> 0 and A11: i2 <> len (GoB f) and A12: LSeg ((f /. k),(f /. (k + 1))) = LSeg (((GoB f) * (i2,(j1 + 1))),((GoB f) * ((i2 + 1),(j1 + 1)))) ; now__::_thesis:_(_(_f_/._k_=_(GoB_f)_*_(i2,(j1_+_1))_&_f_/._(k_+_1)_=_(GoB_f)_*_((i2_+_1),(j1_+_1))_&_Int_(cell_((GoB_f),i2,(j1_+_1)))_c=_(LeftComp_f)_\/_(RightComp_f)_)_or_(_f_/._k_=_(GoB_f)_*_((i2_+_1),(j1_+_1))_&_f_/._(k_+_1)_=_(GoB_f)_*_(i2,(j1_+_1))_&_Int_(cell_((GoB_f),i2,(j1_+_1)))_c=_(LeftComp_f)_\/_(RightComp_f)_)_) percases ( ( f /. k = (GoB f) * (i2,(j1 + 1)) & f /. (k + 1) = (GoB f) * ((i2 + 1),(j1 + 1)) ) or ( f /. k = (GoB f) * ((i2 + 1),(j1 + 1)) & f /. (k + 1) = (GoB f) * (i2,(j1 + 1)) ) ) by A12, SPPOL_1:8; caseA13: ( f /. k = (GoB f) * (i2,(j1 + 1)) & f /. (k + 1) = (GoB f) * ((i2 + 1),(j1 + 1)) ) ; ::_thesis: Int (cell ((GoB f),i2,(j1 + 1))) c= (LeftComp f) \/ (RightComp f) A14: ( Int (left_cell (f,k)) c= LeftComp f & LeftComp f c= (LeftComp f) \/ (RightComp f) ) by A9, GOBOARD9:21, XBOOLE_1:7; i2 < len (GoB f) by A3, A11, XXREAL_0:1; then A15: i2 + 1 <= len (GoB f) by NAT_1:13; 0 + 1 <= j1 + 1 by XREAL_1:6; then A16: ( Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] & j1 + 1 in Seg (width (GoB f)) ) by A4, A8, FINSEQ_1:1, MATRIX_1:def_4; 1 <= i2 + 1 by NAT_1:11; then i2 + 1 in dom (GoB f) by A15, FINSEQ_3:25; then A17: [(i2 + 1),(j1 + 1)] in Indices (GoB f) by A16, ZFMISC_1:87; i2 >= 0 + 1 by A10, NAT_1:13; then i2 in dom (GoB f) by A3, FINSEQ_3:25; then [i2,(j1 + 1)] in Indices (GoB f) by A16, ZFMISC_1:87; then left_cell (f,k) = cell ((GoB f),i2,(j1 + 1)) by A9, A13, A17, GOBOARD5:28; hence Int (cell ((GoB f),i2,(j1 + 1))) c= (LeftComp f) \/ (RightComp f) by A14, XBOOLE_1:1; ::_thesis: verum end; caseA18: ( f /. k = (GoB f) * ((i2 + 1),(j1 + 1)) & f /. (k + 1) = (GoB f) * (i2,(j1 + 1)) ) ; ::_thesis: Int (cell ((GoB f),i2,(j1 + 1))) c= (LeftComp f) \/ (RightComp f) A19: ( Int (right_cell (f,k)) c= RightComp f & RightComp f c= (LeftComp f) \/ (RightComp f) ) by A9, GOBOARD9:25, XBOOLE_1:7; i2 < len (GoB f) by A3, A11, XXREAL_0:1; then A20: i2 + 1 <= len (GoB f) by NAT_1:13; 0 + 1 <= j1 + 1 by XREAL_1:6; then A21: ( Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] & j1 + 1 in Seg (width (GoB f)) ) by A4, A8, FINSEQ_1:1, MATRIX_1:def_4; 1 <= i2 + 1 by NAT_1:11; then i2 + 1 in dom (GoB f) by A20, FINSEQ_3:25; then A22: [(i2 + 1),(j1 + 1)] in Indices (GoB f) by A21, ZFMISC_1:87; i2 >= 0 + 1 by A10, NAT_1:13; then i2 in dom (GoB f) by A3, FINSEQ_3:25; then [i2,(j1 + 1)] in Indices (GoB f) by A21, ZFMISC_1:87; then right_cell (f,k) = cell ((GoB f),i2,(j1 + 1)) by A9, A18, A22, GOBOARD5:29; hence Int (cell ((GoB f),i2,(j1 + 1))) c= (LeftComp f) \/ (RightComp f) by A19, XBOOLE_1:1; ::_thesis: verum end; end; end; hence Int (cell ((GoB f),i2,(j1 + 1))) c= (LeftComp f) \/ (RightComp f) ; ::_thesis: verum end; caseA23: for k being Element of NAT holds ( not 1 <= k or not k + 1 <= len f or not i2 <> 0 or not i2 <> len (GoB f) or not LSeg ((f /. k),(f /. (k + 1))) = LSeg (((GoB f) * (i2,(j1 + 1))),((GoB f) * ((i2 + 1),(j1 + 1)))) ) ; ::_thesis: Int (cell ((GoB f),i2,(j1 + 1))) c= (LeftComp f) \/ (RightComp f) now__::_thesis:_(_(_i2_=_0_&_Int_(cell_((GoB_f),i2,(j1_+_1)))_c=_(LeftComp_f)_\/_(RightComp_f)_)_or_(_i2_=_len_(GoB_f)_&_Int_(cell_((GoB_f),i2,(j1_+_1)))_c=_(LeftComp_f)_\/_(RightComp_f)_)_or_(_i2_<>_0_&_i2_<>_len_(GoB_f)_&_(_for_k_being_Element_of_NAT_holds_ (_not_1_<=_k_or_not_k_+_1_<=_len_f_or_not_LSeg_((f_/._k),(f_/._(k_+_1)))_=_LSeg_(((GoB_f)_*_(i2,(j1_+_1))),((GoB_f)_*_((i2_+_1),(j1_+_1))))_)_)_&_Int_(cell_((GoB_f),i2,(j1_+_1)))_c=_(LeftComp_f)_\/_(RightComp_f)_)_) percases ( i2 = 0 or i2 = len (GoB f) or ( i2 <> 0 & i2 <> len (GoB f) & ( for k being Element of NAT holds ( not 1 <= k or not k + 1 <= len f or not LSeg ((f /. k),(f /. (k + 1))) = LSeg (((GoB f) * (i2,(j1 + 1))),((GoB f) * ((i2 + 1),(j1 + 1)))) ) ) ) ) by A23; caseA24: i2 = 0 ; ::_thesis: Int (cell ((GoB f),i2,(j1 + 1))) c= (LeftComp f) \/ (RightComp f) reconsider p = |[((((GoB f) * (1,(j1 + 1))) `1) - 1),(((GoB f) * (1,(j1 + 1))) `2)]| as Point of (TOP-REAL 2) ; A25: 1 < len (GoB f) by GOBOARD7:32; A26: 1 < width (GoB f) by GOBOARD7:33; reconsider P = {p} as Subset of (TOP-REAL 2) ; A27: p `1 < (p `1) + 1 by XREAL_1:29; A28: 1 <= 1 + j1 by NAT_1:11; then ((GoB f) * (1,(j1 + 1))) `1 = ((GoB f) * (1,1)) `1 by A4, A8, A25, GOBOARD5:2; then A29: p `1 = (((GoB f) * (1,1)) `1) - 1 by EUCLID:52; p in { |[s,r]| where s, r is Real : s <= ((GoB f) * (1,1)) `1 } proof p = |[(p `1),(p `2)]| by EUCLID:53; hence p in { |[s,r]| where s, r is Real : s <= ((GoB f) * (1,1)) `1 } by A29, A27; ::_thesis: verum end; then A30: p in v_strip ((GoB f),i2) by A24, A26, GOBOARD5:10; ( ( for q being Point of (TOP-REAL 2) st q in P holds q `1 < ((GoB f) * (1,1)) `1 ) implies P misses L~ f ) by GOBOARD8:21; then A31: ( p in {p} & {p} c= (L~ f) ` ) by A29, A27, SUBSET_1:23, TARSKI:def_1; then reconsider p1 = p as Point of ((TOP-REAL 2) | ((L~ f) `)) by PRE_TOPC:8; A32: ( j1 = 0 or j1 >= 0 + 1 ) by NAT_1:13; A33: now__::_thesis:_(_(_j1_>=_1_&_j1_+_1_<_width_(GoB_f)_&_p_in_(cell_((GoB_f),i2,(j1_+_1)))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i2,j1))_/\_((L~_f)_`)_)_or_(_j1_>=_1_&_j1_+_1_=_width_(GoB_f)_&_p_in_(cell_((GoB_f),i2,(j1_+_1)))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i2,j1))_/\_((L~_f)_`)_)_or_(_j1_=_0_&_j1_+_1_<_width_(GoB_f)_&_p_in_(cell_((GoB_f),i2,(j1_+_1)))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i2,j1))_/\_((L~_f)_`)_)_or_(_j1_=_0_&_j1_+_1_=_width_(GoB_f)_&_p_in_(cell_((GoB_f),i2,(j1_+_1)))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i2,j1))_/\_((L~_f)_`)_)_) percases ( ( j1 >= 1 & j1 + 1 < width (GoB f) ) or ( j1 >= 1 & j1 + 1 = width (GoB f) ) or ( j1 = 0 & j1 + 1 < width (GoB f) ) or ( j1 = 0 & j1 + 1 = width (GoB f) ) ) by A4, A8, A32, XXREAL_0:1; caseA34: ( j1 >= 1 & j1 + 1 < width (GoB f) ) ; ::_thesis: ( p in (cell ((GoB f),i2,(j1 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j1)) /\ ((L~ f) `) ) then A35: (j1 + 1) + 1 <= width (GoB f) by NAT_1:13; A36: p in { |[s,r]| where s, r is Real : ( ((GoB f) * (1,(j1 + 1))) `2 <= r & r <= ((GoB f) * (1,((j1 + 1) + 1))) `2 ) } proof j1 + 1 < (j1 + 1) + 1 by NAT_1:13; then ((GoB f) * (1,(j1 + 1))) `2 <= ((GoB f) * (1,((j1 + 1) + 1))) `2 by A25, A28, A35, GOBOARD5:4; hence p in { |[s,r]| where s, r is Real : ( ((GoB f) * (1,(j1 + 1))) `2 <= r & r <= ((GoB f) * (1,((j1 + 1) + 1))) `2 ) } ; ::_thesis: verum end; 1 <= j1 + 1 by NAT_1:11; then p in h_strip ((GoB f),(j1 + 1)) by A25, A34, A36, GOBOARD5:5; then p in (h_strip ((GoB f),(j1 + 1))) /\ (v_strip ((GoB f),i2)) by A30, XBOOLE_0:def_4; then A37: p in cell ((GoB f),i2,(j1 + 1)) by GOBOARD5:def_3; A38: p in { |[s,r]| where s, r is Real : ( ((GoB f) * (1,j1)) `2 <= r & r <= ((GoB f) * (1,(j1 + 1))) `2 ) } proof j1 < j1 + 1 by NAT_1:13; then ((GoB f) * (1,j1)) `2 < ((GoB f) * (1,(j1 + 1))) `2 by A25, A34, GOBOARD5:4; hence p in { |[s,r]| where s, r is Real : ( ((GoB f) * (1,j1)) `2 <= r & r <= ((GoB f) * (1,(j1 + 1))) `2 ) } ; ::_thesis: verum end; j1 < width (GoB f) by A34, NAT_1:13; then p in h_strip ((GoB f),j1) by A25, A34, A38, GOBOARD5:5; then p in (h_strip ((GoB f),j1)) /\ (v_strip ((GoB f),i2)) by A30, XBOOLE_0:def_4; then p in cell ((GoB f),i2,j1) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),i2,(j1 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j1)) /\ ((L~ f) `) ) by A31, A37, XBOOLE_0:def_4; ::_thesis: verum end; caseA39: ( j1 >= 1 & j1 + 1 = width (GoB f) ) ; ::_thesis: ( p in (cell ((GoB f),i2,(j1 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j1)) /\ ((L~ f) `) ) A40: j1 < j1 + 1 by NAT_1:13; A41: p in { |[s,r]| where s, r is Real : ( ((GoB f) * (1,j1)) `2 <= r & r <= ((GoB f) * (1,(j1 + 1))) `2 ) } proof ((GoB f) * (1,j1)) `2 < ((GoB f) * (1,(j1 + 1))) `2 by A25, A39, A40, GOBOARD5:4; hence p in { |[s,r]| where s, r is Real : ( ((GoB f) * (1,j1)) `2 <= r & r <= ((GoB f) * (1,(j1 + 1))) `2 ) } ; ::_thesis: verum end; p in { |[s,r]| where s, r is Real : ((GoB f) * (1,(j1 + 1))) `2 <= r } ; then p in h_strip ((GoB f),(j1 + 1)) by A25, A39, GOBOARD5:6; then p in (h_strip ((GoB f),(j1 + 1))) /\ (v_strip ((GoB f),i2)) by A30, XBOOLE_0:def_4; then A42: p in cell ((GoB f),i2,(j1 + 1)) by GOBOARD5:def_3; j1 < width (GoB f) by A39, NAT_1:13; then p in h_strip ((GoB f),j1) by A25, A39, A41, GOBOARD5:5; then p in (h_strip ((GoB f),j1)) /\ (v_strip ((GoB f),i2)) by A30, XBOOLE_0:def_4; then p in cell ((GoB f),i2,j1) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),i2,(j1 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j1)) /\ ((L~ f) `) ) by A31, A42, XBOOLE_0:def_4; ::_thesis: verum end; caseA43: ( j1 = 0 & j1 + 1 < width (GoB f) ) ; ::_thesis: ( p in (cell ((GoB f),i2,(j1 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j1)) /\ ((L~ f) `) ) then A44: (j1 + 1) + 1 <= width (GoB f) by NAT_1:13; p in { |[s,r]| where s, r is Real : ( ((GoB f) * (1,(j1 + 1))) `2 <= r & r <= ((GoB f) * (1,((j1 + 1) + 1))) `2 ) } proof j1 + 1 < (j1 + 1) + 1 by NAT_1:13; then ((GoB f) * (1,(j1 + 1))) `2 <= ((GoB f) * (1,((j1 + 1) + 1))) `2 by A25, A28, A44, GOBOARD5:4; hence p in { |[s,r]| where s, r is Real : ( ((GoB f) * (1,(j1 + 1))) `2 <= r & r <= ((GoB f) * (1,((j1 + 1) + 1))) `2 ) } ; ::_thesis: verum end; then p in h_strip ((GoB f),(j1 + 1)) by A25, A43, GOBOARD5:5; then p in (h_strip ((GoB f),(j1 + 1))) /\ (v_strip ((GoB f),i2)) by A30, XBOOLE_0:def_4; then A45: p in cell ((GoB f),i2,(j1 + 1)) by GOBOARD5:def_3; p in { |[s,r]| where s, r is Real : r <= ((GoB f) * (1,1)) `2 } by A43; then p in h_strip ((GoB f),j1) by A25, A43, GOBOARD5:7; then p in (h_strip ((GoB f),j1)) /\ (v_strip ((GoB f),i2)) by A30, XBOOLE_0:def_4; then p in cell ((GoB f),i2,j1) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),i2,(j1 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j1)) /\ ((L~ f) `) ) by A31, A45, XBOOLE_0:def_4; ::_thesis: verum end; caseA46: ( j1 = 0 & j1 + 1 = width (GoB f) ) ; ::_thesis: ( p in (cell ((GoB f),i2,(j1 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j1)) /\ ((L~ f) `) ) p in { |[s,r]| where s, r is Real : ((GoB f) * (1,(j1 + 1))) `2 <= r } ; then p in h_strip ((GoB f),(j1 + 1)) by A25, A46, GOBOARD5:6; then p in (h_strip ((GoB f),(j1 + 1))) /\ (v_strip ((GoB f),i2)) by A30, XBOOLE_0:def_4; then A47: p in cell ((GoB f),i2,(j1 + 1)) by GOBOARD5:def_3; p in { |[s,r]| where s, r is Real : r <= ((GoB f) * (1,1)) `2 } by A46; then p in h_strip ((GoB f),j1) by A25, A46, GOBOARD5:7; then p in (h_strip ((GoB f),j1)) /\ (v_strip ((GoB f),i2)) by A30, XBOOLE_0:def_4; then p in cell ((GoB f),i2,j1) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),i2,(j1 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j1)) /\ ((L~ f) `) ) by A31, A47, XBOOLE_0:def_4; ::_thesis: verum end; end; end; then p in Cl (Down ((Int (cell ((GoB f),i2,(j1 + 1)))),((L~ f) `))) by A3, Th2; then A48: Cl (Down ((Int (cell ((GoB f),i2,(j1 + 1)))),((L~ f) `))) c= Component_of p1 by A3, A4, A8, Th3, GOBRD11:1; Down ((RightComp f),((L~ f) `)) is closed by Lm4, CONNSP_1:33; then A49: Cl (Down ((RightComp f),((L~ f) `))) = Down ((RightComp f),((L~ f) `)) by PRE_TOPC:22; Down ((LeftComp f),((L~ f) `)) is closed by Lm3, CONNSP_1:33; then A50: Cl (Down ((LeftComp f),((L~ f) `))) = Down ((LeftComp f),((L~ f) `)) by PRE_TOPC:22; (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) = Down (((LeftComp f) \/ (RightComp f)),((L~ f) `)) by GOBRD11:4; then A51: Cl (Down (((LeftComp f) \/ (RightComp f)),((L~ f) `))) = (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A50, A49, PRE_TOPC:20; A52: ( Down ((Int (cell ((GoB f),i2,(j1 + 1)))),((L~ f) `)) c= Cl (Down ((Int (cell ((GoB f),i2,(j1 + 1)))),((L~ f) `))) & Down ((Int (cell ((GoB f),i2,(j1 + 1)))),((L~ f) `)) = Int (cell ((GoB f),i2,(j1 + 1))) ) by A3, A4, A8, Th3, PRE_TOPC:18; A53: ( Down ((LeftComp f),((L~ f) `)) = LeftComp f & Down ((RightComp f),((L~ f) `)) = RightComp f ) by Th5; Down ((Int (cell ((GoB f),i2,j1))),((L~ f) `)) c= (LeftComp f) \/ (RightComp f) by A1, A2, A6, A7, Th3; then Down ((Int (cell ((GoB f),i2,j1))),((L~ f) `)) c= Down (((LeftComp f) \/ (RightComp f)),((L~ f) `)) by A53, GOBRD11:4; then A54: Cl (Down ((Int (cell ((GoB f),i2,j1))),((L~ f) `))) c= Cl (Down (((LeftComp f) \/ (RightComp f)),((L~ f) `))) by PRE_TOPC:19; p in Cl (Down ((Int (cell ((GoB f),i2,j1))),((L~ f) `))) by A2, A3, A33, Th2; then Component_of p1 c= (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A54, A51, Th5, CONNSP_3:21; then Cl (Down ((Int (cell ((GoB f),i2,(j1 + 1)))),((L~ f) `))) c= (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A48, XBOOLE_1:1; hence Int (cell ((GoB f),i2,(j1 + 1))) c= (LeftComp f) \/ (RightComp f) by A53, A52, XBOOLE_1:1; ::_thesis: verum end; caseA55: i2 = len (GoB f) ; ::_thesis: Int (cell ((GoB f),i2,(j1 + 1))) c= (LeftComp f) \/ (RightComp f) reconsider p = |[((((GoB f) * ((len (GoB f)),(j1 + 1))) `1) + 1),(((GoB f) * ((len (GoB f)),(j1 + 1))) `2)]| as Point of (TOP-REAL 2) ; A56: 1 < len (GoB f) by GOBOARD7:32; reconsider P = {p} as Subset of (TOP-REAL 2) ; A57: ( ( for q being Point of (TOP-REAL 2) st q in P holds ((GoB f) * ((len (GoB f)),1)) `1 < q `1 ) implies P misses L~ f ) by GOBOARD8:22; A58: 1 < width (GoB f) by GOBOARD7:33; A59: 1 <= 1 + j1 by NAT_1:11; then ((GoB f) * ((len (GoB f)),(j1 + 1))) `1 = ((GoB f) * ((len (GoB f)),1)) `1 by A4, A8, A56, GOBOARD5:2; then A60: p `1 = (((GoB f) * ((len (GoB f)),1)) `1) + 1 by EUCLID:52; then A61: ((GoB f) * ((len (GoB f)),1)) `1 < p `1 by XREAL_1:29; p in { |[s,r]| where s, r is Real : ((GoB f) * ((len (GoB f)),1)) `1 <= s } proof p = |[(p `1),(p `2)]| by EUCLID:53; hence p in { |[s,r]| where s, r is Real : ((GoB f) * ((len (GoB f)),1)) `1 <= s } by A61; ::_thesis: verum end; then A62: p in v_strip ((GoB f),i2) by A55, A58, GOBOARD5:9; ((GoB f) * ((len (GoB f)),1)) `1 < (((GoB f) * ((len (GoB f)),1)) `1) + 1 by XREAL_1:29; then A63: ( p in {p} & {p} c= (L~ f) ` ) by A60, A57, SUBSET_1:23, TARSKI:def_1; then reconsider p1 = p as Point of ((TOP-REAL 2) | ((L~ f) `)) by PRE_TOPC:8; A64: ( j1 = 0 or j1 >= 0 + 1 ) by NAT_1:13; A65: now__::_thesis:_(_(_j1_>=_1_&_j1_+_1_<_width_(GoB_f)_&_p_in_(cell_((GoB_f),i2,(j1_+_1)))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i2,j1))_/\_((L~_f)_`)_)_or_(_j1_>=_1_&_j1_+_1_=_width_(GoB_f)_&_p_in_(cell_((GoB_f),i2,(j1_+_1)))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i2,j1))_/\_((L~_f)_`)_)_or_(_j1_=_0_&_j1_+_1_<_width_(GoB_f)_&_p_in_(cell_((GoB_f),i2,(j1_+_1)))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i2,j1))_/\_((L~_f)_`)_)_or_(_j1_=_0_&_j1_+_1_=_width_(GoB_f)_&_contradiction_)_) percases ( ( j1 >= 1 & j1 + 1 < width (GoB f) ) or ( j1 >= 1 & j1 + 1 = width (GoB f) ) or ( j1 = 0 & j1 + 1 < width (GoB f) ) or ( j1 = 0 & j1 + 1 = width (GoB f) ) ) by A4, A8, A64, XXREAL_0:1; caseA66: ( j1 >= 1 & j1 + 1 < width (GoB f) ) ; ::_thesis: ( p in (cell ((GoB f),i2,(j1 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j1)) /\ ((L~ f) `) ) then A67: (j1 + 1) + 1 <= width (GoB f) by NAT_1:13; A68: p in { |[s,r]| where s, r is Real : ( ((GoB f) * ((len (GoB f)),(j1 + 1))) `2 <= r & r <= ((GoB f) * ((len (GoB f)),((j1 + 1) + 1))) `2 ) } proof j1 + 1 < (j1 + 1) + 1 by NAT_1:13; then ((GoB f) * ((len (GoB f)),(j1 + 1))) `2 <= ((GoB f) * ((len (GoB f)),((j1 + 1) + 1))) `2 by A56, A59, A67, GOBOARD5:4; hence p in { |[s,r]| where s, r is Real : ( ((GoB f) * ((len (GoB f)),(j1 + 1))) `2 <= r & r <= ((GoB f) * ((len (GoB f)),((j1 + 1) + 1))) `2 ) } ; ::_thesis: verum end; 1 <= j1 + 1 by NAT_1:11; then p in h_strip ((GoB f),(j1 + 1)) by A56, A66, A68, GOBOARD5:5; then p in (h_strip ((GoB f),(j1 + 1))) /\ (v_strip ((GoB f),i2)) by A62, XBOOLE_0:def_4; then A69: p in cell ((GoB f),i2,(j1 + 1)) by GOBOARD5:def_3; A70: p in { |[s,r]| where s, r is Real : ( ((GoB f) * ((len (GoB f)),j1)) `2 <= r & r <= ((GoB f) * ((len (GoB f)),(j1 + 1))) `2 ) } proof j1 < j1 + 1 by NAT_1:13; then ((GoB f) * ((len (GoB f)),j1)) `2 < ((GoB f) * ((len (GoB f)),(j1 + 1))) `2 by A56, A66, GOBOARD5:4; hence p in { |[s,r]| where s, r is Real : ( ((GoB f) * ((len (GoB f)),j1)) `2 <= r & r <= ((GoB f) * ((len (GoB f)),(j1 + 1))) `2 ) } ; ::_thesis: verum end; j1 < width (GoB f) by A66, NAT_1:13; then p in h_strip ((GoB f),j1) by A56, A66, A70, GOBOARD5:5; then p in (h_strip ((GoB f),j1)) /\ (v_strip ((GoB f),i2)) by A62, XBOOLE_0:def_4; then p in cell ((GoB f),i2,j1) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),i2,(j1 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j1)) /\ ((L~ f) `) ) by A63, A69, XBOOLE_0:def_4; ::_thesis: verum end; caseA71: ( j1 >= 1 & j1 + 1 = width (GoB f) ) ; ::_thesis: ( p in (cell ((GoB f),i2,(j1 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j1)) /\ ((L~ f) `) ) A72: j1 < j1 + 1 by NAT_1:13; A73: p in { |[s,r]| where s, r is Real : ( ((GoB f) * ((len (GoB f)),j1)) `2 <= r & r <= ((GoB f) * ((len (GoB f)),(j1 + 1))) `2 ) } proof ((GoB f) * ((len (GoB f)),j1)) `2 < ((GoB f) * ((len (GoB f)),(j1 + 1))) `2 by A56, A71, A72, GOBOARD5:4; hence p in { |[s,r]| where s, r is Real : ( ((GoB f) * ((len (GoB f)),j1)) `2 <= r & r <= ((GoB f) * ((len (GoB f)),(j1 + 1))) `2 ) } ; ::_thesis: verum end; p in { |[s,r]| where s, r is Real : ((GoB f) * ((len (GoB f)),(j1 + 1))) `2 <= r } ; then p in h_strip ((GoB f),(j1 + 1)) by A56, A71, GOBOARD5:6; then p in (h_strip ((GoB f),(j1 + 1))) /\ (v_strip ((GoB f),i2)) by A62, XBOOLE_0:def_4; then A74: p in cell ((GoB f),i2,(j1 + 1)) by GOBOARD5:def_3; j1 < width (GoB f) by A71, NAT_1:13; then p in h_strip ((GoB f),j1) by A56, A71, A73, GOBOARD5:5; then p in (h_strip ((GoB f),j1)) /\ (v_strip ((GoB f),i2)) by A62, XBOOLE_0:def_4; then p in cell ((GoB f),i2,j1) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),i2,(j1 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j1)) /\ ((L~ f) `) ) by A63, A74, XBOOLE_0:def_4; ::_thesis: verum end; caseA75: ( j1 = 0 & j1 + 1 < width (GoB f) ) ; ::_thesis: ( p in (cell ((GoB f),i2,(j1 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j1)) /\ ((L~ f) `) ) then A76: (j1 + 1) + 1 <= width (GoB f) by NAT_1:13; p in { |[s,r]| where s, r is Real : ( ((GoB f) * ((len (GoB f)),(j1 + 1))) `2 <= r & r <= ((GoB f) * ((len (GoB f)),((j1 + 1) + 1))) `2 ) } proof j1 + 1 < (j1 + 1) + 1 by NAT_1:13; then ((GoB f) * ((len (GoB f)),(j1 + 1))) `2 <= ((GoB f) * ((len (GoB f)),((j1 + 1) + 1))) `2 by A56, A59, A76, GOBOARD5:4; hence p in { |[s,r]| where s, r is Real : ( ((GoB f) * ((len (GoB f)),(j1 + 1))) `2 <= r & r <= ((GoB f) * ((len (GoB f)),((j1 + 1) + 1))) `2 ) } ; ::_thesis: verum end; then p in h_strip ((GoB f),(j1 + 1)) by A56, A75, GOBOARD5:5; then p in (h_strip ((GoB f),(j1 + 1))) /\ (v_strip ((GoB f),i2)) by A62, XBOOLE_0:def_4; then A77: p in cell ((GoB f),i2,(j1 + 1)) by GOBOARD5:def_3; p in { |[s,r]| where s, r is Real : r <= ((GoB f) * ((len (GoB f)),1)) `2 } by A75; then p in h_strip ((GoB f),j1) by A56, A75, GOBOARD5:7; then p in (h_strip ((GoB f),j1)) /\ (v_strip ((GoB f),i2)) by A62, XBOOLE_0:def_4; then p in cell ((GoB f),i2,j1) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),i2,(j1 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j1)) /\ ((L~ f) `) ) by A63, A77, XBOOLE_0:def_4; ::_thesis: verum end; case ( j1 = 0 & j1 + 1 = width (GoB f) ) ; ::_thesis: contradiction hence contradiction by GOBOARD7:33; ::_thesis: verum end; end; end; then p in Cl (Down ((Int (cell ((GoB f),i2,(j1 + 1)))),((L~ f) `))) by A3, Th2; then A78: Cl (Down ((Int (cell ((GoB f),i2,(j1 + 1)))),((L~ f) `))) c= Component_of p1 by A3, A4, A8, Th3, GOBRD11:1; Down ((RightComp f),((L~ f) `)) is closed by Lm4, CONNSP_1:33; then A79: Cl (Down ((RightComp f),((L~ f) `))) = Down ((RightComp f),((L~ f) `)) by PRE_TOPC:22; Down ((LeftComp f),((L~ f) `)) is closed by Lm3, CONNSP_1:33; then A80: Cl (Down ((LeftComp f),((L~ f) `))) = Down ((LeftComp f),((L~ f) `)) by PRE_TOPC:22; (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) = Down (((LeftComp f) \/ (RightComp f)),((L~ f) `)) by GOBRD11:4; then A81: Cl (Down (((LeftComp f) \/ (RightComp f)),((L~ f) `))) = (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A80, A79, PRE_TOPC:20; A82: ( Down ((Int (cell ((GoB f),i2,(j1 + 1)))),((L~ f) `)) c= Cl (Down ((Int (cell ((GoB f),i2,(j1 + 1)))),((L~ f) `))) & Down ((Int (cell ((GoB f),i2,(j1 + 1)))),((L~ f) `)) = Int (cell ((GoB f),i2,(j1 + 1))) ) by A3, A4, A8, Th3, PRE_TOPC:18; A83: ( Down ((LeftComp f),((L~ f) `)) = LeftComp f & Down ((RightComp f),((L~ f) `)) = RightComp f ) by Th5; Down ((Int (cell ((GoB f),i2,j1))),((L~ f) `)) c= (LeftComp f) \/ (RightComp f) by A1, A2, A6, A7, Th3; then Down ((Int (cell ((GoB f),i2,j1))),((L~ f) `)) c= Down (((LeftComp f) \/ (RightComp f)),((L~ f) `)) by A83, GOBRD11:4; then A84: Cl (Down ((Int (cell ((GoB f),i2,j1))),((L~ f) `))) c= Cl (Down (((LeftComp f) \/ (RightComp f)),((L~ f) `))) by PRE_TOPC:19; p in Cl (Down ((Int (cell ((GoB f),i2,j1))),((L~ f) `))) by A2, A3, A65, Th2; then Component_of p1 c= (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A84, A81, Th5, CONNSP_3:21; then Cl (Down ((Int (cell ((GoB f),i2,(j1 + 1)))),((L~ f) `))) c= (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A78, XBOOLE_1:1; hence Int (cell ((GoB f),i2,(j1 + 1))) c= (LeftComp f) \/ (RightComp f) by A83, A82, XBOOLE_1:1; ::_thesis: verum end; caseA85: ( i2 <> 0 & i2 <> len (GoB f) & ( for k being Element of NAT holds ( not 1 <= k or not k + 1 <= len f or not LSeg ((f /. k),(f /. (k + 1))) = LSeg (((GoB f) * (i2,(j1 + 1))),((GoB f) * ((i2 + 1),(j1 + 1)))) ) ) ) ; ::_thesis: Int (cell ((GoB f),i2,(j1 + 1))) c= (LeftComp f) \/ (RightComp f) then A86: i2 < len (GoB f) by A3, XXREAL_0:1; then A87: i2 + 1 <= len (GoB f) by NAT_1:13; for k being Element of NAT st 1 <= k & k + 1 <= len f holds LSeg (((GoB f) * (i2,(j1 + 1))),((GoB f) * ((i2 + 1),(j1 + 1)))) <> LSeg (f,k) proof let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f implies LSeg (((GoB f) * (i2,(j1 + 1))),((GoB f) * ((i2 + 1),(j1 + 1)))) <> LSeg (f,k) ) assume A88: ( 1 <= k & k + 1 <= len f ) ; ::_thesis: LSeg (((GoB f) * (i2,(j1 + 1))),((GoB f) * ((i2 + 1),(j1 + 1)))) <> LSeg (f,k) then LSeg (f,k) = LSeg ((f /. k),(f /. (k + 1))) by TOPREAL1:def_3; hence LSeg (((GoB f) * (i2,(j1 + 1))),((GoB f) * ((i2 + 1),(j1 + 1)))) <> LSeg (f,k) by A85, A88; ::_thesis: verum end; then A89: ( 1 <= j1 + 1 & j1 + 1 <= width (GoB f) & 1 <= i2 & i2 + 1 <= len (GoB f) implies not (1 / 2) * (((GoB f) * (i2,(j1 + 1))) + ((GoB f) * ((i2 + 1),(j1 + 1)))) in L~ f ) by GOBOARD7:40; reconsider p = (1 / 2) * (((GoB f) * (i2,(j1 + 1))) + ((GoB f) * ((i2 + 1),(j1 + 1)))) as Point of (TOP-REAL 2) ; A90: p `1 = (1 / 2) * ((((GoB f) * (i2,(j1 + 1))) + ((GoB f) * ((i2 + 1),(j1 + 1)))) `1) by TOPREAL3:4 .= (1 / 2) * ((((GoB f) * (i2,(j1 + 1))) `1) + (((GoB f) * ((i2 + 1),(j1 + 1))) `1)) by TOPREAL3:2 ; reconsider P = {p} as Subset of (TOP-REAL 2) ; A91: 1 < len (GoB f) by GOBOARD7:32; Down ((RightComp f),((L~ f) `)) is closed by Lm4, CONNSP_1:33; then A92: Cl (Down ((RightComp f),((L~ f) `))) = Down ((RightComp f),((L~ f) `)) by PRE_TOPC:22; Down ((LeftComp f),((L~ f) `)) is closed by Lm3, CONNSP_1:33; then A93: Cl (Down ((LeftComp f),((L~ f) `))) = Down ((LeftComp f),((L~ f) `)) by PRE_TOPC:22; (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) = Down (((LeftComp f) \/ (RightComp f)),((L~ f) `)) by GOBRD11:4; then A94: Cl (Down (((LeftComp f) \/ (RightComp f)),((L~ f) `))) = (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A93, A92, PRE_TOPC:20; A95: ( Down ((LeftComp f),((L~ f) `)) = LeftComp f & Down ((RightComp f),((L~ f) `)) = RightComp f ) by Th5; Down ((Int (cell ((GoB f),i2,j1))),((L~ f) `)) c= (LeftComp f) \/ (RightComp f) by A1, A2, A6, A7, Th3; then Down ((Int (cell ((GoB f),i2,j1))),((L~ f) `)) c= Down (((LeftComp f) \/ (RightComp f)),((L~ f) `)) by A95, GOBRD11:4; then A96: Cl (Down ((Int (cell ((GoB f),i2,j1))),((L~ f) `))) c= Cl (Down (((LeftComp f) \/ (RightComp f)),((L~ f) `))) by PRE_TOPC:19; A97: ( Down ((Int (cell ((GoB f),i2,(j1 + 1)))),((L~ f) `)) c= Cl (Down ((Int (cell ((GoB f),i2,(j1 + 1)))),((L~ f) `))) & Down ((Int (cell ((GoB f),i2,(j1 + 1)))),((L~ f) `)) = Int (cell ((GoB f),i2,(j1 + 1))) ) by A3, A4, A8, Th3, PRE_TOPC:18; A98: 1 <= j1 + 1 by NAT_1:11; A99: 0 + 1 <= i2 by A85, NAT_1:13; then A100: 1 < i2 + 1 by NAT_1:13; ( ( for x being set st x in P holds not x in L~ f ) implies P misses L~ f ) by XBOOLE_0:3; then A101: ( p in {p} & {p} c= (L~ f) ` ) by A4, A8, A99, A86, A89, NAT_1:13, SUBSET_1:23, TARSKI:def_1; then reconsider p1 = p as Point of ((TOP-REAL 2) | ((L~ f) `)) by PRE_TOPC:8; A102: 1 <= 1 + j1 by NAT_1:11; p `2 = (1 / 2) * ((((GoB f) * (i2,(j1 + 1))) + ((GoB f) * ((i2 + 1),(j1 + 1)))) `2) by TOPREAL3:4 .= (1 / 2) * ((((GoB f) * (i2,(j1 + 1))) `2) + (((GoB f) * ((i2 + 1),(j1 + 1))) `2)) by TOPREAL3:2 ; then A103: p = |[((1 / 2) * ((((GoB f) * (i2,(j1 + 1))) `1) + (((GoB f) * ((i2 + 1),(j1 + 1))) `1))),((1 / 2) * ((((GoB f) * (i2,(j1 + 1))) `2) + (((GoB f) * ((i2 + 1),(j1 + 1))) `2)))]| by A90, EUCLID:53; i2 < i2 + 1 by NAT_1:13; then A104: ((GoB f) * (i2,(j1 + 1))) `1 < ((GoB f) * ((i2 + 1),(j1 + 1))) `1 by A4, A8, A99, A87, A102, GOBOARD5:3; then (((GoB f) * (i2,(j1 + 1))) `1) + (((GoB f) * ((i2 + 1),(j1 + 1))) `1) < (((GoB f) * ((i2 + 1),(j1 + 1))) `1) + (((GoB f) * ((i2 + 1),(j1 + 1))) `1) by XREAL_1:8; then A105: ((((GoB f) * (i2,(j1 + 1))) `1) + (((GoB f) * ((i2 + 1),(j1 + 1))) `1)) / 2 < ((((GoB f) * ((i2 + 1),(j1 + 1))) `1) + (((GoB f) * ((i2 + 1),(j1 + 1))) `1)) / 2 by XREAL_1:74; (((GoB f) * (i2,(j1 + 1))) `1) + (((GoB f) * (i2,(j1 + 1))) `1) < (((GoB f) * (i2,(j1 + 1))) `1) + (((GoB f) * ((i2 + 1),(j1 + 1))) `1) by A104, XREAL_1:8; then A106: ((((GoB f) * (i2,(j1 + 1))) `1) + (((GoB f) * (i2,(j1 + 1))) `1)) / 2 < ((((GoB f) * (i2,(j1 + 1))) `1) + (((GoB f) * ((i2 + 1),(j1 + 1))) `1)) / 2 by XREAL_1:74; p in { |[s,r]| where s, r is Real : ( ((GoB f) * (i2,(j1 + 1))) `1 <= s & s <= ((GoB f) * ((i2 + 1),(j1 + 1))) `1 ) } proof p = |[(p `1),(p `2)]| by EUCLID:53; hence p in { |[s,r]| where s, r is Real : ( ((GoB f) * (i2,(j1 + 1))) `1 <= s & s <= ((GoB f) * ((i2 + 1),(j1 + 1))) `1 ) } by A90, A106, A105; ::_thesis: verum end; then A107: p in v_strip ((GoB f),i2) by A4, A8, A99, A86, A98, GOBOARD5:8; A108: ( j1 = 0 or j1 >= 0 + 1 ) by NAT_1:13; A109: now__::_thesis:_(_(_j1_>=_1_&_j1_+_1_<_width_(GoB_f)_&_p_in_(cell_((GoB_f),i2,(j1_+_1)))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i2,j1))_/\_((L~_f)_`)_)_or_(_j1_>=_1_&_j1_+_1_=_width_(GoB_f)_&_p_in_(cell_((GoB_f),i2,(j1_+_1)))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i2,j1))_/\_((L~_f)_`)_)_or_(_j1_=_0_&_j1_+_1_<_width_(GoB_f)_&_p_in_(cell_((GoB_f),i2,(j1_+_1)))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i2,j1))_/\_((L~_f)_`)_)_or_(_j1_=_0_&_j1_+_1_=_width_(GoB_f)_&_contradiction_)_) percases ( ( j1 >= 1 & j1 + 1 < width (GoB f) ) or ( j1 >= 1 & j1 + 1 = width (GoB f) ) or ( j1 = 0 & j1 + 1 < width (GoB f) ) or ( j1 = 0 & j1 + 1 = width (GoB f) ) ) by A4, A8, A108, XXREAL_0:1; caseA110: ( j1 >= 1 & j1 + 1 < width (GoB f) ) ; ::_thesis: ( p in (cell ((GoB f),i2,(j1 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j1)) /\ ((L~ f) `) ) then A111: (j1 + 1) + 1 <= width (GoB f) by NAT_1:13; A112: p in { |[s,r]| where s, r is Real : ( ((GoB f) * (1,(j1 + 1))) `2 <= r & r <= ((GoB f) * (1,((j1 + 1) + 1))) `2 ) } proof j1 + 1 < (j1 + 1) + 1 by NAT_1:13; then A113: ((GoB f) * (1,(j1 + 1))) `2 < ((GoB f) * (1,((j1 + 1) + 1))) `2 by A91, A102, A111, GOBOARD5:4; ( ((GoB f) * (i2,(j1 + 1))) `2 = ((GoB f) * (1,(j1 + 1))) `2 & ((GoB f) * ((i2 + 1),(j1 + 1))) `2 = ((GoB f) * (1,(j1 + 1))) `2 ) by A3, A4, A8, A99, A87, A102, A100, GOBOARD5:1; hence p in { |[s,r]| where s, r is Real : ( ((GoB f) * (1,(j1 + 1))) `2 <= r & r <= ((GoB f) * (1,((j1 + 1) + 1))) `2 ) } by A103, A113; ::_thesis: verum end; 1 <= j1 + 1 by NAT_1:11; then p in h_strip ((GoB f),(j1 + 1)) by A91, A110, A112, GOBOARD5:5; then p in (h_strip ((GoB f),(j1 + 1))) /\ (v_strip ((GoB f),i2)) by A107, XBOOLE_0:def_4; then A114: p in cell ((GoB f),i2,(j1 + 1)) by GOBOARD5:def_3; A115: p in { |[s,r]| where s, r is Real : ( ((GoB f) * (1,j1)) `2 <= r & r <= ((GoB f) * (1,(j1 + 1))) `2 ) } proof j1 < j1 + 1 by NAT_1:13; then A116: ((GoB f) * (1,j1)) `2 < ((GoB f) * (1,(j1 + 1))) `2 by A91, A110, GOBOARD5:4; ( ((GoB f) * (i2,(j1 + 1))) `2 = ((GoB f) * (1,(j1 + 1))) `2 & ((GoB f) * ((i2 + 1),(j1 + 1))) `2 = ((GoB f) * (1,(j1 + 1))) `2 ) by A3, A4, A8, A99, A87, A102, A100, GOBOARD5:1; hence p in { |[s,r]| where s, r is Real : ( ((GoB f) * (1,j1)) `2 <= r & r <= ((GoB f) * (1,(j1 + 1))) `2 ) } by A103, A116; ::_thesis: verum end; j1 < width (GoB f) by A110, NAT_1:13; then p in h_strip ((GoB f),j1) by A91, A110, A115, GOBOARD5:5; then p in (h_strip ((GoB f),j1)) /\ (v_strip ((GoB f),i2)) by A107, XBOOLE_0:def_4; then p in cell ((GoB f),i2,j1) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),i2,(j1 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j1)) /\ ((L~ f) `) ) by A101, A114, XBOOLE_0:def_4; ::_thesis: verum end; caseA117: ( j1 >= 1 & j1 + 1 = width (GoB f) ) ; ::_thesis: ( p in (cell ((GoB f),i2,(j1 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j1)) /\ ((L~ f) `) ) A118: j1 < j1 + 1 by NAT_1:13; p in { |[s,r]| where s, r is Real : ( ((GoB f) * (1,j1)) `2 <= r & r <= ((GoB f) * (1,(j1 + 1))) `2 ) } proof A119: ((GoB f) * (1,j1)) `2 < ((GoB f) * (1,(j1 + 1))) `2 by A91, A117, A118, GOBOARD5:4; ( ((GoB f) * (i2,(j1 + 1))) `2 = ((GoB f) * (1,(j1 + 1))) `2 & ((GoB f) * ((i2 + 1),(j1 + 1))) `2 = ((GoB f) * (1,(j1 + 1))) `2 ) by A3, A4, A8, A99, A87, A102, A100, GOBOARD5:1; hence p in { |[s,r]| where s, r is Real : ( ((GoB f) * (1,j1)) `2 <= r & r <= ((GoB f) * (1,(j1 + 1))) `2 ) } by A103, A119; ::_thesis: verum end; then p in h_strip ((GoB f),j1) by A91, A117, A118, GOBOARD5:5; then p in (h_strip ((GoB f),j1)) /\ (v_strip ((GoB f),i2)) by A107, XBOOLE_0:def_4; then A120: p in cell ((GoB f),i2,j1) by GOBOARD5:def_3; p in { |[s,r]| where s, r is Real : ((GoB f) * (1,(j1 + 1))) `2 <= r } proof ( ((GoB f) * (i2,(j1 + 1))) `2 = ((GoB f) * (1,(j1 + 1))) `2 & ((GoB f) * ((i2 + 1),(j1 + 1))) `2 = ((GoB f) * (1,(j1 + 1))) `2 ) by A3, A4, A8, A99, A87, A102, A100, GOBOARD5:1; hence p in { |[s,r]| where s, r is Real : ((GoB f) * (1,(j1 + 1))) `2 <= r } by A103; ::_thesis: verum end; then p in h_strip ((GoB f),(j1 + 1)) by A91, A117, GOBOARD5:6; then p in (h_strip ((GoB f),(j1 + 1))) /\ (v_strip ((GoB f),i2)) by A107, XBOOLE_0:def_4; then p in cell ((GoB f),i2,(j1 + 1)) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),i2,(j1 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j1)) /\ ((L~ f) `) ) by A101, A120, XBOOLE_0:def_4; ::_thesis: verum end; caseA121: ( j1 = 0 & j1 + 1 < width (GoB f) ) ; ::_thesis: ( p in (cell ((GoB f),i2,(j1 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j1)) /\ ((L~ f) `) ) then A122: (j1 + 1) + 1 <= width (GoB f) by NAT_1:13; p in { |[s,r]| where s, r is Real : ( ((GoB f) * (1,(j1 + 1))) `2 <= r & r <= ((GoB f) * (1,((j1 + 1) + 1))) `2 ) } proof j1 + 1 < (j1 + 1) + 1 by NAT_1:13; then A123: ((GoB f) * (1,(j1 + 1))) `2 < ((GoB f) * (1,((j1 + 1) + 1))) `2 by A91, A102, A122, GOBOARD5:4; ( ((GoB f) * (i2,(j1 + 1))) `2 = ((GoB f) * (1,(j1 + 1))) `2 & ((GoB f) * ((i2 + 1),(j1 + 1))) `2 = ((GoB f) * (1,(j1 + 1))) `2 ) by A3, A4, A8, A99, A87, A102, A100, GOBOARD5:1; hence p in { |[s,r]| where s, r is Real : ( ((GoB f) * (1,(j1 + 1))) `2 <= r & r <= ((GoB f) * (1,((j1 + 1) + 1))) `2 ) } by A103, A123; ::_thesis: verum end; then p in h_strip ((GoB f),(j1 + 1)) by A91, A121, GOBOARD5:5; then p in (h_strip ((GoB f),(j1 + 1))) /\ (v_strip ((GoB f),i2)) by A107, XBOOLE_0:def_4; then A124: p in cell ((GoB f),i2,(j1 + 1)) by GOBOARD5:def_3; p in { |[s,r]| where s, r is Real : r <= ((GoB f) * (1,1)) `2 } proof ( ((GoB f) * (i2,(j1 + 1))) `2 = ((GoB f) * (1,(j1 + 1))) `2 & ((GoB f) * ((i2 + 1),(j1 + 1))) `2 = ((GoB f) * (1,(j1 + 1))) `2 ) by A3, A4, A8, A99, A87, A102, A100, GOBOARD5:1; hence p in { |[s,r]| where s, r is Real : r <= ((GoB f) * (1,1)) `2 } by A103, A121; ::_thesis: verum end; then p in h_strip ((GoB f),j1) by A91, A121, GOBOARD5:7; then p in (h_strip ((GoB f),j1)) /\ (v_strip ((GoB f),i2)) by A107, XBOOLE_0:def_4; then p in cell ((GoB f),i2,j1) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),i2,(j1 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j1)) /\ ((L~ f) `) ) by A101, A124, XBOOLE_0:def_4; ::_thesis: verum end; case ( j1 = 0 & j1 + 1 = width (GoB f) ) ; ::_thesis: contradiction hence contradiction by GOBOARD7:33; ::_thesis: verum end; end; end; then p in Cl (Down ((Int (cell ((GoB f),i2,(j1 + 1)))),((L~ f) `))) by A3, Th2; then A125: Cl (Down ((Int (cell ((GoB f),i2,(j1 + 1)))),((L~ f) `))) c= Component_of p1 by A3, A4, A8, Th3, GOBRD11:1; p in Cl (Down ((Int (cell ((GoB f),i2,j1))),((L~ f) `))) by A2, A3, A109, Th2; then Component_of p1 c= (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A96, A94, Th5, CONNSP_3:21; then Cl (Down ((Int (cell ((GoB f),i2,(j1 + 1)))),((L~ f) `))) c= (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A125, XBOOLE_1:1; hence Int (cell ((GoB f),i2,(j1 + 1))) c= (LeftComp f) \/ (RightComp f) by A95, A97, XBOOLE_1:1; ::_thesis: verum end; end; end; hence Int (cell ((GoB f),i2,(j1 + 1))) c= (LeftComp f) \/ (RightComp f) ; ::_thesis: verum end; end; end; hence Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) by A8; ::_thesis: verum end; caseA126: j1 = j2 + 1 ; ::_thesis: Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) then j2 < j1 by NAT_1:13; then A127: j1 -' 1 < j1 by A126, NAT_D:34; A128: j2 < j2 + 1 by NAT_1:13; A129: 1 <= (j1 -' 1) + 1 by NAT_1:11; A130: j2 + 1 < (j2 + 1) + 1 by NAT_1:13; A131: ( 1 <= j1 & j1 -' 1 = j1 - 1 ) by A126, NAT_1:11, XREAL_0:def_2; A132: 1 <= j2 + 1 by NAT_1:11; A133: j1 -' 1 = j2 by A126, NAT_D:34; now__::_thesis:_(_(_ex_k_being_Element_of_NAT_st_ (_1_<=_k_&_k_+_1_<=_len_f_&_i2_<>_0_&_i2_<>_len_(GoB_f)_&_LSeg_((f_/._k),(f_/._(k_+_1)))_=_LSeg_(((GoB_f)_*_(i2,(j2_+_1))),((GoB_f)_*_((i2_+_1),(j2_+_1))))_)_&_Int_(cell_((GoB_f),i2,j2))_c=_(LeftComp_f)_\/_(RightComp_f)_)_or_(_(_for_k_being_Element_of_NAT_holds_ (_not_1_<=_k_or_not_k_+_1_<=_len_f_or_not_i2_<>_0_or_not_i2_<>_len_(GoB_f)_or_not_LSeg_((f_/._k),(f_/._(k_+_1)))_=_LSeg_(((GoB_f)_*_(i2,(j2_+_1))),((GoB_f)_*_((i2_+_1),(j2_+_1))))_)_)_&_Int_(cell_((GoB_f),i2,j2))_c=_(LeftComp_f)_\/_(RightComp_f)_)_) percases ( ex k being Element of NAT st ( 1 <= k & k + 1 <= len f & i2 <> 0 & i2 <> len (GoB f) & LSeg ((f /. k),(f /. (k + 1))) = LSeg (((GoB f) * (i2,(j2 + 1))),((GoB f) * ((i2 + 1),(j2 + 1)))) ) or for k being Element of NAT holds ( not 1 <= k or not k + 1 <= len f or not i2 <> 0 or not i2 <> len (GoB f) or not LSeg ((f /. k),(f /. (k + 1))) = LSeg (((GoB f) * (i2,(j2 + 1))),((GoB f) * ((i2 + 1),(j2 + 1)))) ) ) ; case ex k being Element of NAT st ( 1 <= k & k + 1 <= len f & i2 <> 0 & i2 <> len (GoB f) & LSeg ((f /. k),(f /. (k + 1))) = LSeg (((GoB f) * (i2,(j2 + 1))),((GoB f) * ((i2 + 1),(j2 + 1)))) ) ; ::_thesis: Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) then consider k being Element of NAT such that A134: ( 1 <= k & k + 1 <= len f ) and A135: i2 <> 0 and A136: i2 <> len (GoB f) and A137: LSeg ((f /. k),(f /. (k + 1))) = LSeg (((GoB f) * (i2,((j1 -' 1) + 1))),((GoB f) * ((i2 + 1),((j1 -' 1) + 1)))) by A133; now__::_thesis:_(_(_f_/._k_=_(GoB_f)_*_(i2,((j1_-'_1)_+_1))_&_f_/._(k_+_1)_=_(GoB_f)_*_((i2_+_1),((j1_-'_1)_+_1))_&_Int_(cell_((GoB_f),i2,(j1_-'_1)))_c=_(LeftComp_f)_\/_(RightComp_f)_)_or_(_f_/._k_=_(GoB_f)_*_((i2_+_1),((j1_-'_1)_+_1))_&_f_/._(k_+_1)_=_(GoB_f)_*_(i2,((j1_-'_1)_+_1))_&_Int_(cell_((GoB_f),i2,(j1_-'_1)))_c=_(LeftComp_f)_\/_(RightComp_f)_)_) percases ( ( f /. k = (GoB f) * (i2,((j1 -' 1) + 1)) & f /. (k + 1) = (GoB f) * ((i2 + 1),((j1 -' 1) + 1)) ) or ( f /. k = (GoB f) * ((i2 + 1),((j1 -' 1) + 1)) & f /. (k + 1) = (GoB f) * (i2,((j1 -' 1) + 1)) ) ) by A137, SPPOL_1:8; caseA138: ( f /. k = (GoB f) * (i2,((j1 -' 1) + 1)) & f /. (k + 1) = (GoB f) * ((i2 + 1),((j1 -' 1) + 1)) ) ; ::_thesis: Int (cell ((GoB f),i2,(j1 -' 1))) c= (LeftComp f) \/ (RightComp f) A139: ( Int (right_cell (f,k)) c= RightComp f & RightComp f c= (LeftComp f) \/ (RightComp f) ) by A134, GOBOARD9:25, XBOOLE_1:7; i2 < len (GoB f) by A3, A136, XXREAL_0:1; then A140: i2 + 1 <= len (GoB f) by NAT_1:13; j1 -' 1 < width (GoB f) by A2, A127, XXREAL_0:2; then (j1 -' 1) + 1 <= width (GoB f) by NAT_1:13; then A141: ( Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] & (j1 -' 1) + 1 in Seg (width (GoB f)) ) by A129, FINSEQ_1:1, MATRIX_1:def_4; 1 <= i2 + 1 by NAT_1:11; then i2 + 1 in dom (GoB f) by A140, FINSEQ_3:25; then A142: [(i2 + 1),((j1 -' 1) + 1)] in Indices (GoB f) by A141, ZFMISC_1:87; i2 >= 0 + 1 by A135, NAT_1:13; then i2 in dom (GoB f) by A3, FINSEQ_3:25; then [i2,((j1 -' 1) + 1)] in Indices (GoB f) by A141, ZFMISC_1:87; then right_cell (f,k) = cell ((GoB f),i2,(j1 -' 1)) by A134, A138, A142, GOBOARD5:28; hence Int (cell ((GoB f),i2,(j1 -' 1))) c= (LeftComp f) \/ (RightComp f) by A139, XBOOLE_1:1; ::_thesis: verum end; caseA143: ( f /. k = (GoB f) * ((i2 + 1),((j1 -' 1) + 1)) & f /. (k + 1) = (GoB f) * (i2,((j1 -' 1) + 1)) ) ; ::_thesis: Int (cell ((GoB f),i2,(j1 -' 1))) c= (LeftComp f) \/ (RightComp f) A144: ( Int (left_cell (f,k)) c= LeftComp f & LeftComp f c= (LeftComp f) \/ (RightComp f) ) by A134, GOBOARD9:21, XBOOLE_1:7; i2 < len (GoB f) by A3, A136, XXREAL_0:1; then A145: i2 + 1 <= len (GoB f) by NAT_1:13; A146: ( Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] & (j1 -' 1) + 1 in Seg (width (GoB f)) ) by A2, A131, FINSEQ_1:1, MATRIX_1:def_4; 1 <= i2 + 1 by NAT_1:11; then i2 + 1 in dom (GoB f) by A145, FINSEQ_3:25; then A147: [(i2 + 1),((j1 -' 1) + 1)] in Indices (GoB f) by A146, ZFMISC_1:87; i2 >= 0 + 1 by A135, NAT_1:13; then i2 in dom (GoB f) by A3, FINSEQ_3:25; then [i2,((j1 -' 1) + 1)] in Indices (GoB f) by A146, ZFMISC_1:87; then left_cell (f,k) = cell ((GoB f),i2,(j1 -' 1)) by A134, A143, A147, GOBOARD5:29; hence Int (cell ((GoB f),i2,(j1 -' 1))) c= (LeftComp f) \/ (RightComp f) by A144, XBOOLE_1:1; ::_thesis: verum end; end; end; hence Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) by A126, NAT_D:34; ::_thesis: verum end; caseA148: for k being Element of NAT holds ( not 1 <= k or not k + 1 <= len f or not i2 <> 0 or not i2 <> len (GoB f) or not LSeg ((f /. k),(f /. (k + 1))) = LSeg (((GoB f) * (i2,(j2 + 1))),((GoB f) * ((i2 + 1),(j2 + 1)))) ) ; ::_thesis: Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) now__::_thesis:_(_(_i2_=_0_&_Int_(cell_((GoB_f),i2,j2))_c=_(LeftComp_f)_\/_(RightComp_f)_)_or_(_i2_=_len_(GoB_f)_&_Int_(cell_((GoB_f),i2,j2))_c=_(LeftComp_f)_\/_(RightComp_f)_)_or_(_i2_<>_0_&_i2_<>_len_(GoB_f)_&_(_for_k_being_Element_of_NAT_holds_ (_not_1_<=_k_or_not_k_+_1_<=_len_f_or_not_LSeg_((f_/._k),(f_/._(k_+_1)))_=_LSeg_(((GoB_f)_*_(i2,(j2_+_1))),((GoB_f)_*_((i2_+_1),(j2_+_1))))_)_)_&_Int_(cell_((GoB_f),i2,j2))_c=_(LeftComp_f)_\/_(RightComp_f)_)_) percases ( i2 = 0 or i2 = len (GoB f) or ( i2 <> 0 & i2 <> len (GoB f) & ( for k being Element of NAT holds ( not 1 <= k or not k + 1 <= len f or not LSeg ((f /. k),(f /. (k + 1))) = LSeg (((GoB f) * (i2,(j2 + 1))),((GoB f) * ((i2 + 1),(j2 + 1)))) ) ) ) ) by A148; caseA149: i2 = 0 ; ::_thesis: Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) reconsider p = |[((((GoB f) * (1,(j2 + 1))) `1) - 1),(((GoB f) * (1,(j2 + 1))) `2)]| as Point of (TOP-REAL 2) ; A150: 1 < len (GoB f) by GOBOARD7:32; A151: 1 < width (GoB f) by GOBOARD7:33; reconsider P = {p} as Subset of (TOP-REAL 2) ; A152: p `1 < (p `1) + 1 by XREAL_1:29; A153: 1 <= j2 + 1 by NAT_1:11; then ((GoB f) * (1,(j2 + 1))) `1 = ((GoB f) * (1,1)) `1 by A2, A126, A150, GOBOARD5:2; then A154: p `1 = (((GoB f) * (1,1)) `1) - 1 by EUCLID:52; p in { |[s,r]| where s, r is Real : s <= ((GoB f) * (1,1)) `1 } proof p = |[(p `1),(p `2)]| by EUCLID:53; hence p in { |[s,r]| where s, r is Real : s <= ((GoB f) * (1,1)) `1 } by A154, A152; ::_thesis: verum end; then A155: p in v_strip ((GoB f),i2) by A149, A151, GOBOARD5:10; ( ( for q being Point of (TOP-REAL 2) st q in P holds q `1 < ((GoB f) * (1,1)) `1 ) implies P misses L~ f ) by GOBOARD8:21; then A156: ( p in {p} & {p} c= (L~ f) ` ) by A154, A152, SUBSET_1:23, TARSKI:def_1; then reconsider p1 = p as Point of ((TOP-REAL 2) | ((L~ f) `)) by PRE_TOPC:8; A157: now__::_thesis:_(_(_j2_+_1_<_width_(GoB_f)_&_j2_>_0_&_p_in_(cell_((GoB_f),i2,(j2_+_1)))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i2,j2))_/\_((L~_f)_`)_)_or_(_j2_+_1_<_width_(GoB_f)_&_j2_=_0_&_p_in_(cell_((GoB_f),i2,(j2_+_1)))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i2,j2))_/\_((L~_f)_`)_)_or_(_j2_+_1_=_width_(GoB_f)_&_j2_>_0_&_p_in_(cell_((GoB_f),i2,(j2_+_1)))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i2,j2))_/\_((L~_f)_`)_)_or_(_j2_+_1_=_width_(GoB_f)_&_j2_=_0_&_p_in_(cell_((GoB_f),i2,(j2_+_1)))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i2,j2))_/\_((L~_f)_`)_)_) percases ( ( j2 + 1 < width (GoB f) & j2 > 0 ) or ( j2 + 1 < width (GoB f) & j2 = 0 ) or ( j2 + 1 = width (GoB f) & j2 > 0 ) or ( j2 + 1 = width (GoB f) & j2 = 0 ) ) by A2, A126, XXREAL_0:1; caseA158: ( j2 + 1 < width (GoB f) & j2 > 0 ) ; ::_thesis: ( p in (cell ((GoB f),i2,(j2 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) then A159: (j2 + 1) + 1 <= width (GoB f) by NAT_1:13; A160: p in { |[s,r]| where s, r is Real : ( ((GoB f) * (1,(j2 + 1))) `2 <= r & r <= ((GoB f) * (1,((j2 + 1) + 1))) `2 ) } proof j2 + 1 < (j2 + 1) + 1 by NAT_1:13; then ((GoB f) * (1,(j2 + 1))) `2 <= ((GoB f) * (1,((j2 + 1) + 1))) `2 by A150, A153, A159, GOBOARD5:4; hence p in { |[s,r]| where s, r is Real : ( ((GoB f) * (1,(j2 + 1))) `2 <= r & r <= ((GoB f) * (1,((j2 + 1) + 1))) `2 ) } ; ::_thesis: verum end; A161: 0 + 1 <= j2 by A158, NAT_1:13; A162: p in { |[s,r]| where s, r is Real : ( ((GoB f) * (1,j2)) `2 <= r & r <= ((GoB f) * (1,(j2 + 1))) `2 ) } proof j2 < j2 + 1 by NAT_1:13; then ((GoB f) * (1,j2)) `2 < ((GoB f) * (1,(j2 + 1))) `2 by A2, A126, A150, A161, GOBOARD5:4; hence p in { |[s,r]| where s, r is Real : ( ((GoB f) * (1,j2)) `2 <= r & r <= ((GoB f) * (1,(j2 + 1))) `2 ) } ; ::_thesis: verum end; j2 < width (GoB f) by A158, NAT_1:13; then p in h_strip ((GoB f),j2) by A150, A161, A162, GOBOARD5:5; then p in (h_strip ((GoB f),j2)) /\ (v_strip ((GoB f),i2)) by A155, XBOOLE_0:def_4; then A163: p in cell ((GoB f),i2,j2) by GOBOARD5:def_3; 1 <= j2 + 1 by A161, NAT_1:13; then p in h_strip ((GoB f),(j2 + 1)) by A150, A158, A160, GOBOARD5:5; then p in (h_strip ((GoB f),(j2 + 1))) /\ (v_strip ((GoB f),i2)) by A155, XBOOLE_0:def_4; then p in cell ((GoB f),i2,(j2 + 1)) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),i2,(j2 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) by A156, A163, XBOOLE_0:def_4; ::_thesis: verum end; caseA164: ( j2 + 1 < width (GoB f) & j2 = 0 ) ; ::_thesis: ( p in (cell ((GoB f),i2,(j2 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) A165: j2 + 1 < (j2 + 1) + 1 by NAT_1:13; A166: (j2 + 1) + 1 <= width (GoB f) by A164, NAT_1:13; p in { |[s,r]| where s, r is Real : ( ((GoB f) * (1,(j2 + 1))) `2 <= r & r <= ((GoB f) * (1,((j2 + 1) + 1))) `2 ) } proof ((GoB f) * (1,(j2 + 1))) `2 < ((GoB f) * (1,((j2 + 1) + 1))) `2 by A132, A150, A166, A165, GOBOARD5:4; hence p in { |[s,r]| where s, r is Real : ( ((GoB f) * (1,(j2 + 1))) `2 <= r & r <= ((GoB f) * (1,((j2 + 1) + 1))) `2 ) } ; ::_thesis: verum end; then p in h_strip ((GoB f),(j2 + 1)) by A150, A164, GOBOARD5:5; then p in (h_strip ((GoB f),(j2 + 1))) /\ (v_strip ((GoB f),i2)) by A155, XBOOLE_0:def_4; then A167: p in cell ((GoB f),i2,(j2 + 1)) by GOBOARD5:def_3; p in { |[s,r]| where s, r is Real : r <= ((GoB f) * (1,(j2 + 1))) `2 } ; then p in h_strip ((GoB f),j2) by A150, A164, GOBOARD5:7; then p in (h_strip ((GoB f),j2)) /\ (v_strip ((GoB f),i2)) by A155, XBOOLE_0:def_4; then p in cell ((GoB f),i2,j2) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),i2,(j2 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) by A156, A167, XBOOLE_0:def_4; ::_thesis: verum end; caseA168: ( j2 + 1 = width (GoB f) & j2 > 0 ) ; ::_thesis: ( p in (cell ((GoB f),i2,(j2 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) then A169: 0 + 1 <= j2 by NAT_1:13; A170: p in { |[s,r]| where s, r is Real : ( ((GoB f) * (1,j2)) `2 <= r & r <= ((GoB f) * (1,(j2 + 1))) `2 ) } proof ((GoB f) * (1,j2)) `2 < ((GoB f) * (1,(j2 + 1))) `2 by A128, A150, A168, A169, GOBOARD5:4; hence p in { |[s,r]| where s, r is Real : ( ((GoB f) * (1,j2)) `2 <= r & r <= ((GoB f) * (1,(j2 + 1))) `2 ) } ; ::_thesis: verum end; p in { |[s,r]| where s, r is Real : ((GoB f) * (1,(j2 + 1))) `2 <= r } ; then p in h_strip ((GoB f),(j2 + 1)) by A150, A168, GOBOARD5:6; then p in (h_strip ((GoB f),(j2 + 1))) /\ (v_strip ((GoB f),i2)) by A155, XBOOLE_0:def_4; then A171: p in cell ((GoB f),i2,(j2 + 1)) by GOBOARD5:def_3; j2 < width (GoB f) by A168, NAT_1:13; then p in h_strip ((GoB f),j2) by A150, A169, A170, GOBOARD5:5; then p in (h_strip ((GoB f),j2)) /\ (v_strip ((GoB f),i2)) by A155, XBOOLE_0:def_4; then p in cell ((GoB f),i2,j2) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),i2,(j2 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) by A156, A171, XBOOLE_0:def_4; ::_thesis: verum end; caseA172: ( j2 + 1 = width (GoB f) & j2 = 0 ) ; ::_thesis: ( p in (cell ((GoB f),i2,(j2 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) p in { |[s,r]| where s, r is Real : ((GoB f) * (1,(j2 + 1))) `2 <= r } ; then p in h_strip ((GoB f),(j2 + 1)) by A150, A172, GOBOARD5:6; then p in (h_strip ((GoB f),(j2 + 1))) /\ (v_strip ((GoB f),i2)) by A155, XBOOLE_0:def_4; then A173: p in cell ((GoB f),i2,(j2 + 1)) by GOBOARD5:def_3; p in { |[s,r]| where s, r is Real : r <= ((GoB f) * (1,1)) `2 } by A172; then p in h_strip ((GoB f),j2) by A150, A172, GOBOARD5:7; then p in (h_strip ((GoB f),j2)) /\ (v_strip ((GoB f),i2)) by A155, XBOOLE_0:def_4; then p in cell ((GoB f),i2,j2) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),i2,(j2 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) by A156, A173, XBOOLE_0:def_4; ::_thesis: verum end; end; end; then p in Cl (Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `))) by A3, A4, Th2; then A174: Cl (Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `))) c= Component_of p1 by A3, A4, Th3, GOBRD11:1; Down ((RightComp f),((L~ f) `)) is closed by Lm4, CONNSP_1:33; then A175: Cl (Down ((RightComp f),((L~ f) `))) = Down ((RightComp f),((L~ f) `)) by PRE_TOPC:22; Down ((LeftComp f),((L~ f) `)) is closed by Lm3, CONNSP_1:33; then A176: Cl (Down ((LeftComp f),((L~ f) `))) = Down ((LeftComp f),((L~ f) `)) by PRE_TOPC:22; A177: ( Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `)) c= Cl (Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `))) & Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `)) = Int (cell ((GoB f),i2,j2)) ) by A3, A4, Th3, PRE_TOPC:18; (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) = Down (((LeftComp f) \/ (RightComp f)),((L~ f) `)) by GOBRD11:4; then A178: Cl (Down (((LeftComp f) \/ (RightComp f)),((L~ f) `))) = (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A176, A175, PRE_TOPC:20; A179: ( Down ((LeftComp f),((L~ f) `)) = LeftComp f & Down ((RightComp f),((L~ f) `)) = RightComp f ) by Th5; Down ((Int (cell ((GoB f),i2,j1))),((L~ f) `)) c= (LeftComp f) \/ (RightComp f) by A1, A2, A6, A7, Th3; then Down ((Int (cell ((GoB f),i2,j1))),((L~ f) `)) c= Down (((LeftComp f) \/ (RightComp f)),((L~ f) `)) by A179, GOBRD11:4; then A180: Cl (Down ((Int (cell ((GoB f),i2,j1))),((L~ f) `))) c= Cl (Down (((LeftComp f) \/ (RightComp f)),((L~ f) `))) by PRE_TOPC:19; p in Cl (Down ((Int (cell ((GoB f),i2,(j2 + 1)))),((L~ f) `))) by A3, A157, Th2; then Component_of p1 c= (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A126, A180, A178, Th5, CONNSP_3:21; then Cl (Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `))) c= (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A174, XBOOLE_1:1; hence Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) by A179, A177, XBOOLE_1:1; ::_thesis: verum end; caseA181: i2 = len (GoB f) ; ::_thesis: Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) reconsider p = |[((((GoB f) * ((len (GoB f)),(j2 + 1))) `1) + 1),(((GoB f) * ((len (GoB f)),(j2 + 1))) `2)]| as Point of (TOP-REAL 2) ; A182: 1 < len (GoB f) by GOBOARD7:32; reconsider P = {p} as Subset of (TOP-REAL 2) ; A183: ( ( for q being Point of (TOP-REAL 2) st q in P holds ((GoB f) * ((len (GoB f)),1)) `1 < q `1 ) implies P misses L~ f ) by GOBOARD8:22; A184: 1 < width (GoB f) by GOBOARD7:33; 1 <= j2 + 1 by NAT_1:11; then ((GoB f) * ((len (GoB f)),(j2 + 1))) `1 = ((GoB f) * ((len (GoB f)),1)) `1 by A2, A126, A182, GOBOARD5:2; then A185: p `1 = (((GoB f) * ((len (GoB f)),1)) `1) + 1 by EUCLID:52; then A186: ((GoB f) * ((len (GoB f)),1)) `1 < p `1 by XREAL_1:29; p in { |[s,r]| where s, r is Real : ((GoB f) * ((len (GoB f)),1)) `1 <= s } proof p = |[(p `1),(p `2)]| by EUCLID:53; hence p in { |[s,r]| where s, r is Real : ((GoB f) * ((len (GoB f)),1)) `1 <= s } by A186; ::_thesis: verum end; then A187: p in v_strip ((GoB f),i2) by A181, A184, GOBOARD5:9; ((GoB f) * ((len (GoB f)),1)) `1 < (((GoB f) * ((len (GoB f)),1)) `1) + 1 by XREAL_1:29; then A188: ( p in {p} & {p} c= (L~ f) ` ) by A185, A183, SUBSET_1:23, TARSKI:def_1; then reconsider p1 = p as Point of ((TOP-REAL 2) | ((L~ f) `)) by PRE_TOPC:8; A189: now__::_thesis:_(_(_j2_+_1_<_width_(GoB_f)_&_j2_>_0_&_p_in_(cell_((GoB_f),i2,(j2_+_1)))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i2,j2))_/\_((L~_f)_`)_)_or_(_j2_+_1_<_width_(GoB_f)_&_j2_=_0_&_p_in_(cell_((GoB_f),i2,(j2_+_1)))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i2,j2))_/\_((L~_f)_`)_)_or_(_j2_+_1_=_width_(GoB_f)_&_j2_>_0_&_p_in_(cell_((GoB_f),i2,(j2_+_1)))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i2,j2))_/\_((L~_f)_`)_)_or_(_j2_+_1_=_width_(GoB_f)_&_j2_=_0_&_contradiction_)_) percases ( ( j2 + 1 < width (GoB f) & j2 > 0 ) or ( j2 + 1 < width (GoB f) & j2 = 0 ) or ( j2 + 1 = width (GoB f) & j2 > 0 ) or ( j2 + 1 = width (GoB f) & j2 = 0 ) ) by A2, A126, XXREAL_0:1; caseA190: ( j2 + 1 < width (GoB f) & j2 > 0 ) ; ::_thesis: ( p in (cell ((GoB f),i2,(j2 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) then A191: (j2 + 1) + 1 <= width (GoB f) by NAT_1:13; A192: p in { |[s,r]| where s, r is Real : ( ((GoB f) * ((len (GoB f)),(j2 + 1))) `2 <= r & r <= ((GoB f) * ((len (GoB f)),((j2 + 1) + 1))) `2 ) } proof j2 + 1 < (j2 + 1) + 1 by NAT_1:13; then ((GoB f) * ((len (GoB f)),(j2 + 1))) `2 <= ((GoB f) * ((len (GoB f)),((j2 + 1) + 1))) `2 by A132, A182, A191, GOBOARD5:4; hence p in { |[s,r]| where s, r is Real : ( ((GoB f) * ((len (GoB f)),(j2 + 1))) `2 <= r & r <= ((GoB f) * ((len (GoB f)),((j2 + 1) + 1))) `2 ) } ; ::_thesis: verum end; 1 <= j2 + 1 by NAT_1:11; then p in h_strip ((GoB f),(j2 + 1)) by A182, A190, A192, GOBOARD5:5; then p in (h_strip ((GoB f),(j2 + 1))) /\ (v_strip ((GoB f),i2)) by A187, XBOOLE_0:def_4; then A193: p in cell ((GoB f),i2,(j2 + 1)) by GOBOARD5:def_3; A194: 0 + 1 <= j2 by A190, NAT_1:13; A195: j2 < j2 + 1 by NAT_1:13; A196: p in { |[s,r]| where s, r is Real : ( ((GoB f) * ((len (GoB f)),j2)) `2 <= r & r <= ((GoB f) * ((len (GoB f)),(j2 + 1))) `2 ) } proof ((GoB f) * ((len (GoB f)),j2)) `2 < ((GoB f) * ((len (GoB f)),(j2 + 1))) `2 by A2, A126, A182, A194, A195, GOBOARD5:4; hence p in { |[s,r]| where s, r is Real : ( ((GoB f) * ((len (GoB f)),j2)) `2 <= r & r <= ((GoB f) * ((len (GoB f)),(j2 + 1))) `2 ) } ; ::_thesis: verum end; j2 < width (GoB f) by A190, NAT_1:13; then p in h_strip ((GoB f),j2) by A182, A194, A196, GOBOARD5:5; then p in (h_strip ((GoB f),j2)) /\ (v_strip ((GoB f),i2)) by A187, XBOOLE_0:def_4; then p in cell ((GoB f),i2,j2) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),i2,(j2 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) by A188, A193, XBOOLE_0:def_4; ::_thesis: verum end; caseA197: ( j2 + 1 < width (GoB f) & j2 = 0 ) ; ::_thesis: ( p in (cell ((GoB f),i2,(j2 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) then A198: (j2 + 1) + 1 <= width (GoB f) by NAT_1:13; p in { |[s,r]| where s, r is Real : ( ((GoB f) * ((len (GoB f)),(j2 + 1))) `2 <= r & r <= ((GoB f) * ((len (GoB f)),((j2 + 1) + 1))) `2 ) } proof ((GoB f) * ((len (GoB f)),(j2 + 1))) `2 < ((GoB f) * ((len (GoB f)),((j2 + 1) + 1))) `2 by A132, A130, A182, A198, GOBOARD5:4; hence p in { |[s,r]| where s, r is Real : ( ((GoB f) * ((len (GoB f)),(j2 + 1))) `2 <= r & r <= ((GoB f) * ((len (GoB f)),((j2 + 1) + 1))) `2 ) } ; ::_thesis: verum end; then p in h_strip ((GoB f),(j2 + 1)) by A182, A197, GOBOARD5:5; then p in (h_strip ((GoB f),(j2 + 1))) /\ (v_strip ((GoB f),i2)) by A187, XBOOLE_0:def_4; then A199: p in cell ((GoB f),i2,(j2 + 1)) by GOBOARD5:def_3; p in { |[s,r]| where s, r is Real : r <= ((GoB f) * ((len (GoB f)),1)) `2 } by A197; then p in h_strip ((GoB f),j2) by A182, A197, GOBOARD5:7; then p in (h_strip ((GoB f),j2)) /\ (v_strip ((GoB f),i2)) by A187, XBOOLE_0:def_4; then p in cell ((GoB f),i2,j2) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),i2,(j2 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) by A188, A199, XBOOLE_0:def_4; ::_thesis: verum end; caseA200: ( j2 + 1 = width (GoB f) & j2 > 0 ) ; ::_thesis: ( p in (cell ((GoB f),i2,(j2 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) then A201: ( 0 + 1 <= j2 & j2 < width (GoB f) ) by NAT_1:13; p in { |[s,r]| where s, r is Real : ( ((GoB f) * ((len (GoB f)),j2)) `2 <= r & r <= ((GoB f) * ((len (GoB f)),(j2 + 1))) `2 ) } proof ((GoB f) * ((len (GoB f)),j2)) `2 <= ((GoB f) * ((len (GoB f)),(j2 + 1))) `2 by A182, A200, A201, GOBOARD5:4; hence p in { |[s,r]| where s, r is Real : ( ((GoB f) * ((len (GoB f)),j2)) `2 <= r & r <= ((GoB f) * ((len (GoB f)),(j2 + 1))) `2 ) } ; ::_thesis: verum end; then p in h_strip ((GoB f),j2) by A182, A201, GOBOARD5:5; then p in (h_strip ((GoB f),j2)) /\ (v_strip ((GoB f),i2)) by A187, XBOOLE_0:def_4; then A202: p in cell ((GoB f),i2,j2) by GOBOARD5:def_3; p in { |[s,r]| where s, r is Real : ((GoB f) * ((len (GoB f)),(width (GoB f)))) `2 <= r } by A200; then p in h_strip ((GoB f),(j2 + 1)) by A182, A200, GOBOARD5:6; then p in (h_strip ((GoB f),(j2 + 1))) /\ (v_strip ((GoB f),i2)) by A187, XBOOLE_0:def_4; then p in cell ((GoB f),i2,(j2 + 1)) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),i2,(j2 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) by A188, A202, XBOOLE_0:def_4; ::_thesis: verum end; case ( j2 + 1 = width (GoB f) & j2 = 0 ) ; ::_thesis: contradiction hence contradiction by GOBOARD7:33; ::_thesis: verum end; end; end; then p in Cl (Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `))) by A3, A4, Th2; then A203: Cl (Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `))) c= Component_of p1 by A3, A4, Th3, GOBRD11:1; Down ((RightComp f),((L~ f) `)) is closed by Lm4, CONNSP_1:33; then A204: Cl (Down ((RightComp f),((L~ f) `))) = Down ((RightComp f),((L~ f) `)) by PRE_TOPC:22; Down ((LeftComp f),((L~ f) `)) is closed by Lm3, CONNSP_1:33; then A205: Cl (Down ((LeftComp f),((L~ f) `))) = Down ((LeftComp f),((L~ f) `)) by PRE_TOPC:22; A206: ( Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `)) c= Cl (Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `))) & Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `)) = Int (cell ((GoB f),i2,j2)) ) by A3, A4, Th3, PRE_TOPC:18; (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) = Down (((LeftComp f) \/ (RightComp f)),((L~ f) `)) by GOBRD11:4; then A207: Cl (Down (((LeftComp f) \/ (RightComp f)),((L~ f) `))) = (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A205, A204, PRE_TOPC:20; A208: ( Down ((LeftComp f),((L~ f) `)) = LeftComp f & Down ((RightComp f),((L~ f) `)) = RightComp f ) by Th5; Down ((Int (cell ((GoB f),i2,j1))),((L~ f) `)) c= (LeftComp f) \/ (RightComp f) by A1, A2, A6, A7, Th3; then Down ((Int (cell ((GoB f),i2,j1))),((L~ f) `)) c= Down (((LeftComp f) \/ (RightComp f)),((L~ f) `)) by A208, GOBRD11:4; then A209: Cl (Down ((Int (cell ((GoB f),i2,j1))),((L~ f) `))) c= Cl (Down (((LeftComp f) \/ (RightComp f)),((L~ f) `))) by PRE_TOPC:19; p in Cl (Down ((Int (cell ((GoB f),i2,(j2 + 1)))),((L~ f) `))) by A3, A189, Th2; then Component_of p1 c= (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A126, A209, A207, Th5, CONNSP_3:21; then Cl (Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `))) c= (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A203, XBOOLE_1:1; hence Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) by A208, A206, XBOOLE_1:1; ::_thesis: verum end; caseA210: ( i2 <> 0 & i2 <> len (GoB f) & ( for k being Element of NAT holds ( not 1 <= k or not k + 1 <= len f or not LSeg ((f /. k),(f /. (k + 1))) = LSeg (((GoB f) * (i2,(j2 + 1))),((GoB f) * ((i2 + 1),(j2 + 1)))) ) ) ) ; ::_thesis: Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) then A211: i2 < len (GoB f) by A3, XXREAL_0:1; then A212: i2 + 1 <= len (GoB f) by NAT_1:13; for k being Element of NAT st 1 <= k & k + 1 <= len f holds LSeg (((GoB f) * (i2,(j2 + 1))),((GoB f) * ((i2 + 1),(j2 + 1)))) <> LSeg (f,k) proof let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f implies LSeg (((GoB f) * (i2,(j2 + 1))),((GoB f) * ((i2 + 1),(j2 + 1)))) <> LSeg (f,k) ) assume A213: ( 1 <= k & k + 1 <= len f ) ; ::_thesis: LSeg (((GoB f) * (i2,(j2 + 1))),((GoB f) * ((i2 + 1),(j2 + 1)))) <> LSeg (f,k) then LSeg (f,k) = LSeg ((f /. k),(f /. (k + 1))) by TOPREAL1:def_3; hence LSeg (((GoB f) * (i2,(j2 + 1))),((GoB f) * ((i2 + 1),(j2 + 1)))) <> LSeg (f,k) by A210, A213; ::_thesis: verum end; then A214: ( 1 <= j2 + 1 & j2 + 1 <= width (GoB f) & 1 <= i2 & i2 + 1 <= len (GoB f) implies not (1 / 2) * (((GoB f) * (i2,(j2 + 1))) + ((GoB f) * ((i2 + 1),(j2 + 1)))) in L~ f ) by GOBOARD7:40; reconsider p = (1 / 2) * (((GoB f) * (i2,(j2 + 1))) + ((GoB f) * ((i2 + 1),(j2 + 1)))) as Point of (TOP-REAL 2) ; A215: p `1 = (1 / 2) * ((((GoB f) * (i2,(j2 + 1))) + ((GoB f) * ((i2 + 1),(j2 + 1)))) `1) by TOPREAL3:4 .= (1 / 2) * ((((GoB f) * (i2,(j2 + 1))) `1) + (((GoB f) * ((i2 + 1),(j2 + 1))) `1)) by TOPREAL3:2 ; reconsider P = {p} as Subset of (TOP-REAL 2) ; A216: 1 < len (GoB f) by GOBOARD7:32; Down ((RightComp f),((L~ f) `)) is closed by Lm4, CONNSP_1:33; then A217: Cl (Down ((RightComp f),((L~ f) `))) = Down ((RightComp f),((L~ f) `)) by PRE_TOPC:22; Down ((LeftComp f),((L~ f) `)) is closed by Lm3, CONNSP_1:33; then A218: Cl (Down ((LeftComp f),((L~ f) `))) = Down ((LeftComp f),((L~ f) `)) by PRE_TOPC:22; (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) = Down (((LeftComp f) \/ (RightComp f)),((L~ f) `)) by GOBRD11:4; then A219: Cl (Down (((LeftComp f) \/ (RightComp f)),((L~ f) `))) = (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A218, A217, PRE_TOPC:20; A220: 1 <= j2 + 1 by NAT_1:11; A221: ( Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `)) c= Cl (Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `))) & Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `)) = Int (cell ((GoB f),i2,j2)) ) by A3, A4, Th3, PRE_TOPC:18; A222: ( Down ((LeftComp f),((L~ f) `)) = LeftComp f & Down ((RightComp f),((L~ f) `)) = RightComp f ) by Th5; Down ((Int (cell ((GoB f),i2,j1))),((L~ f) `)) c= (LeftComp f) \/ (RightComp f) by A1, A2, A6, A7, Th3; then Down ((Int (cell ((GoB f),i2,j1))),((L~ f) `)) c= Down (((LeftComp f) \/ (RightComp f)),((L~ f) `)) by A222, GOBRD11:4; then A223: Cl (Down ((Int (cell ((GoB f),i2,j1))),((L~ f) `))) c= Cl (Down (((LeftComp f) \/ (RightComp f)),((L~ f) `))) by PRE_TOPC:19; A224: 0 + 1 <= i2 by A210, NAT_1:13; then A225: 1 < i2 + 1 by NAT_1:13; ( ( for x being set st x in P holds not x in L~ f ) implies P misses L~ f ) by XBOOLE_0:3; then A226: ( p in {p} & {p} c= (L~ f) ` ) by A2, A126, A224, A211, A214, NAT_1:13, SUBSET_1:23, TARSKI:def_1; then reconsider p1 = p as Point of ((TOP-REAL 2) | ((L~ f) `)) by PRE_TOPC:8; A227: 1 <= 1 + j2 by NAT_1:11; i2 < i2 + 1 by NAT_1:13; then A228: ((GoB f) * (i2,(j2 + 1))) `1 < ((GoB f) * ((i2 + 1),(j2 + 1))) `1 by A2, A126, A224, A212, A220, GOBOARD5:3; then (((GoB f) * (i2,(j2 + 1))) `1) + (((GoB f) * ((i2 + 1),(j2 + 1))) `1) < (((GoB f) * ((i2 + 1),(j2 + 1))) `1) + (((GoB f) * ((i2 + 1),(j2 + 1))) `1) by XREAL_1:8; then A229: ((((GoB f) * (i2,(j2 + 1))) `1) + (((GoB f) * ((i2 + 1),(j2 + 1))) `1)) / 2 < ((((GoB f) * ((i2 + 1),(j2 + 1))) `1) + (((GoB f) * ((i2 + 1),(j2 + 1))) `1)) / 2 by XREAL_1:74; (((GoB f) * (i2,(j2 + 1))) `1) + (((GoB f) * (i2,(j2 + 1))) `1) < (((GoB f) * (i2,(j2 + 1))) `1) + (((GoB f) * ((i2 + 1),(j2 + 1))) `1) by A228, XREAL_1:8; then A230: ((((GoB f) * (i2,(j2 + 1))) `1) + (((GoB f) * (i2,(j2 + 1))) `1)) / 2 < ((((GoB f) * (i2,(j2 + 1))) `1) + (((GoB f) * ((i2 + 1),(j2 + 1))) `1)) / 2 by XREAL_1:74; p in { |[s,r]| where s, r is Real : ( ((GoB f) * (i2,(j2 + 1))) `1 <= s & s <= ((GoB f) * ((i2 + 1),(j2 + 1))) `1 ) } proof p = |[(p `1),(p `2)]| by EUCLID:53; hence p in { |[s,r]| where s, r is Real : ( ((GoB f) * (i2,(j2 + 1))) `1 <= s & s <= ((GoB f) * ((i2 + 1),(j2 + 1))) `1 ) } by A215, A230, A229; ::_thesis: verum end; then A231: p in v_strip ((GoB f),i2) by A2, A126, A224, A211, A227, GOBOARD5:8; p `2 = (1 / 2) * ((((GoB f) * (i2,(j2 + 1))) + ((GoB f) * ((i2 + 1),(j2 + 1)))) `2) by TOPREAL3:4 .= (1 / 2) * ((((GoB f) * (i2,(j2 + 1))) `2) + (((GoB f) * ((i2 + 1),(j2 + 1))) `2)) by TOPREAL3:2 ; then A232: p = |[((1 / 2) * ((((GoB f) * (i2,(j2 + 1))) `1) + (((GoB f) * ((i2 + 1),(j2 + 1))) `1))),((1 / 2) * ((((GoB f) * (i2,(j2 + 1))) `2) + (((GoB f) * ((i2 + 1),(j2 + 1))) `2)))]| by A215, EUCLID:53; A233: ( j2 = 0 or j2 >= 0 + 1 ) by NAT_1:13; A234: now__::_thesis:_(_(_j2_>=_1_&_j2_+_1_<_width_(GoB_f)_&_p_in_(cell_((GoB_f),i2,(j2_+_1)))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i2,j2))_/\_((L~_f)_`)_)_or_(_j2_>=_1_&_j2_+_1_=_width_(GoB_f)_&_p_in_(cell_((GoB_f),i2,(j2_+_1)))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i2,j2))_/\_((L~_f)_`)_)_or_(_j2_=_0_&_j2_+_1_<_width_(GoB_f)_&_p_in_(cell_((GoB_f),i2,(j2_+_1)))_/\_((L~_f)_`)_&_p_in_(cell_((GoB_f),i2,j2))_/\_((L~_f)_`)_)_or_(_j2_=_0_&_j2_+_1_=_width_(GoB_f)_&_contradiction_)_) percases ( ( j2 >= 1 & j2 + 1 < width (GoB f) ) or ( j2 >= 1 & j2 + 1 = width (GoB f) ) or ( j2 = 0 & j2 + 1 < width (GoB f) ) or ( j2 = 0 & j2 + 1 = width (GoB f) ) ) by A2, A126, A233, XXREAL_0:1; caseA235: ( j2 >= 1 & j2 + 1 < width (GoB f) ) ; ::_thesis: ( p in (cell ((GoB f),i2,(j2 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) then A236: (j2 + 1) + 1 <= width (GoB f) by NAT_1:13; p in { |[s,r]| where s, r is Real : ( ((GoB f) * (1,(j2 + 1))) `2 <= r & r <= ((GoB f) * (1,((j2 + 1) + 1))) `2 ) } proof j2 + 1 < (j2 + 1) + 1 by NAT_1:13; then A237: ((GoB f) * (1,(j2 + 1))) `2 < ((GoB f) * (1,((j2 + 1) + 1))) `2 by A216, A220, A236, GOBOARD5:4; ( ((GoB f) * (i2,(j2 + 1))) `2 = ((GoB f) * (1,(j2 + 1))) `2 & ((GoB f) * ((i2 + 1),(j2 + 1))) `2 = ((GoB f) * (1,(j2 + 1))) `2 ) by A2, A3, A126, A224, A212, A220, A225, GOBOARD5:1; hence p in { |[s,r]| where s, r is Real : ( ((GoB f) * (1,(j2 + 1))) `2 <= r & r <= ((GoB f) * (1,((j2 + 1) + 1))) `2 ) } by A232, A237; ::_thesis: verum end; then p in h_strip ((GoB f),(j2 + 1)) by A216, A227, A235, GOBOARD5:5; then p in (h_strip ((GoB f),(j2 + 1))) /\ (v_strip ((GoB f),i2)) by A231, XBOOLE_0:def_4; then A238: p in cell ((GoB f),i2,(j2 + 1)) by GOBOARD5:def_3; A239: p in { |[s,r]| where s, r is Real : ( ((GoB f) * (1,j2)) `2 <= r & r <= ((GoB f) * (1,(j2 + 1))) `2 ) } proof j2 < j2 + 1 by NAT_1:13; then A240: ((GoB f) * (1,j2)) `2 < ((GoB f) * (1,(j2 + 1))) `2 by A216, A235, GOBOARD5:4; ( ((GoB f) * (i2,(j2 + 1))) `2 = ((GoB f) * (1,(j2 + 1))) `2 & ((GoB f) * ((i2 + 1),(j2 + 1))) `2 = ((GoB f) * (1,(j2 + 1))) `2 ) by A2, A3, A126, A224, A212, A220, A225, GOBOARD5:1; hence p in { |[s,r]| where s, r is Real : ( ((GoB f) * (1,j2)) `2 <= r & r <= ((GoB f) * (1,(j2 + 1))) `2 ) } by A232, A240; ::_thesis: verum end; j2 < width (GoB f) by A235, NAT_1:13; then p in h_strip ((GoB f),j2) by A216, A235, A239, GOBOARD5:5; then p in (h_strip ((GoB f),j2)) /\ (v_strip ((GoB f),i2)) by A231, XBOOLE_0:def_4; then p in cell ((GoB f),i2,j2) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),i2,(j2 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) by A226, A238, XBOOLE_0:def_4; ::_thesis: verum end; caseA241: ( j2 >= 1 & j2 + 1 = width (GoB f) ) ; ::_thesis: ( p in (cell ((GoB f),i2,(j2 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) A242: j2 < j2 + 1 by NAT_1:13; p in { |[s,r]| where s, r is Real : ( ((GoB f) * (1,j2)) `2 <= r & r <= ((GoB f) * (1,(j2 + 1))) `2 ) } proof A243: ((GoB f) * (1,j2)) `2 < ((GoB f) * (1,(j2 + 1))) `2 by A216, A241, A242, GOBOARD5:4; ( ((GoB f) * (i2,(j2 + 1))) `2 = ((GoB f) * (1,(j2 + 1))) `2 & ((GoB f) * ((i2 + 1),(j2 + 1))) `2 = ((GoB f) * (1,(j2 + 1))) `2 ) by A2, A3, A126, A224, A212, A220, A225, GOBOARD5:1; hence p in { |[s,r]| where s, r is Real : ( ((GoB f) * (1,j2)) `2 <= r & r <= ((GoB f) * (1,(j2 + 1))) `2 ) } by A232, A243; ::_thesis: verum end; then p in h_strip ((GoB f),j2) by A216, A241, A242, GOBOARD5:5; then p in (h_strip ((GoB f),j2)) /\ (v_strip ((GoB f),i2)) by A231, XBOOLE_0:def_4; then A244: p in cell ((GoB f),i2,j2) by GOBOARD5:def_3; p in { |[s,r]| where s, r is Real : ((GoB f) * (1,(j2 + 1))) `2 <= r } proof ( ((GoB f) * (i2,(j2 + 1))) `2 = ((GoB f) * (1,(j2 + 1))) `2 & ((GoB f) * ((i2 + 1),(j2 + 1))) `2 = ((GoB f) * (1,(j2 + 1))) `2 ) by A2, A3, A126, A224, A212, A220, A225, GOBOARD5:1; hence p in { |[s,r]| where s, r is Real : ((GoB f) * (1,(j2 + 1))) `2 <= r } by A232; ::_thesis: verum end; then p in h_strip ((GoB f),(j2 + 1)) by A216, A241, GOBOARD5:6; then p in (h_strip ((GoB f),(j2 + 1))) /\ (v_strip ((GoB f),i2)) by A231, XBOOLE_0:def_4; then p in cell ((GoB f),i2,(j2 + 1)) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),i2,(j2 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) by A226, A244, XBOOLE_0:def_4; ::_thesis: verum end; caseA245: ( j2 = 0 & j2 + 1 < width (GoB f) ) ; ::_thesis: ( p in (cell ((GoB f),i2,(j2 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) then A246: (j2 + 1) + 1 <= width (GoB f) by NAT_1:13; p in { |[s,r]| where s, r is Real : ( ((GoB f) * (1,(j2 + 1))) `2 <= r & r <= ((GoB f) * (1,((j2 + 1) + 1))) `2 ) } proof j2 + 1 < (j2 + 1) + 1 by NAT_1:13; then A247: ((GoB f) * (1,(j2 + 1))) `2 < ((GoB f) * (1,((j2 + 1) + 1))) `2 by A216, A220, A246, GOBOARD5:4; ( ((GoB f) * (i2,(j2 + 1))) `2 = ((GoB f) * (1,(j2 + 1))) `2 & ((GoB f) * ((i2 + 1),(j2 + 1))) `2 = ((GoB f) * (1,(j2 + 1))) `2 ) by A2, A3, A126, A224, A212, A220, A225, GOBOARD5:1; hence p in { |[s,r]| where s, r is Real : ( ((GoB f) * (1,(j2 + 1))) `2 <= r & r <= ((GoB f) * (1,((j2 + 1) + 1))) `2 ) } by A232, A247; ::_thesis: verum end; then p in h_strip ((GoB f),j1) by A126, A216, A245, GOBOARD5:5; then p in (h_strip ((GoB f),(j2 + 1))) /\ (v_strip ((GoB f),i2)) by A126, A231, XBOOLE_0:def_4; then A248: p in cell ((GoB f),i2,(j2 + 1)) by GOBOARD5:def_3; p in { |[s,r]| where s, r is Real : r <= ((GoB f) * (1,1)) `2 } proof ( ((GoB f) * (i2,(j2 + 1))) `2 = ((GoB f) * (1,(j2 + 1))) `2 & ((GoB f) * ((i2 + 1),(j2 + 1))) `2 = ((GoB f) * (1,(j2 + 1))) `2 ) by A2, A3, A126, A224, A212, A220, A225, GOBOARD5:1; hence p in { |[s,r]| where s, r is Real : r <= ((GoB f) * (1,1)) `2 } by A232, A245; ::_thesis: verum end; then p in h_strip ((GoB f),j2) by A216, A245, GOBOARD5:7; then p in (h_strip ((GoB f),j2)) /\ (v_strip ((GoB f),i2)) by A231, XBOOLE_0:def_4; then p in cell ((GoB f),i2,j2) by GOBOARD5:def_3; hence ( p in (cell ((GoB f),i2,(j2 + 1))) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) by A226, A248, XBOOLE_0:def_4; ::_thesis: verum end; case ( j2 = 0 & j2 + 1 = width (GoB f) ) ; ::_thesis: contradiction hence contradiction by GOBOARD7:33; ::_thesis: verum end; end; end; then p in Cl (Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `))) by A3, A4, Th2; then A249: Cl (Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `))) c= Component_of p1 by A3, A4, Th3, GOBRD11:1; p in Cl (Down ((Int (cell ((GoB f),i2,j1))),((L~ f) `))) by A3, A126, A234, Th2; then Component_of p1 c= (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A223, A219, Th5, CONNSP_3:21; then Cl (Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `))) c= (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A249, XBOOLE_1:1; hence Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) by A222, A221, XBOOLE_1:1; ::_thesis: verum end; end; end; hence Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) ; ::_thesis: verum end; end; end; hence Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) ; ::_thesis: verum end; end; end; hence Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) ; ::_thesis: verum end; hence ( not Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) or Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) ) ; ::_thesis: verum end; theorem Th6: :: GOBRD12:6 for f being non constant standard special_circular_sequence for i1, j1, i2, j2 being Element of NAT st i1 <= len (GoB f) & j1 <= width (GoB f) & i2 <= len (GoB f) & j2 <= width (GoB f) & i1,j1,i2,j2 are_adjacent2 holds ( Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) iff Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) ) proof let f be non constant standard special_circular_sequence; ::_thesis: for i1, j1, i2, j2 being Element of NAT st i1 <= len (GoB f) & j1 <= width (GoB f) & i2 <= len (GoB f) & j2 <= width (GoB f) & i1,j1,i2,j2 are_adjacent2 holds ( Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) iff Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) ) let i1, j1, i2, j2 be Element of NAT ; ::_thesis: ( i1 <= len (GoB f) & j1 <= width (GoB f) & i2 <= len (GoB f) & j2 <= width (GoB f) & i1,j1,i2,j2 are_adjacent2 implies ( Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) iff Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) ) ) assume that A1: ( i1 <= len (GoB f) & j1 <= width (GoB f) ) and A2: i2 <= len (GoB f) and A3: j2 <= width (GoB f) and A4: i1,j1,i2,j2 are_adjacent2 ; ::_thesis: ( Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) iff Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) ) A5: ( ( i1,i2 are_adjacent1 & j1 = j2 ) or ( i1 = i2 & j1,j2 are_adjacent1 ) ) by A4, GOBRD10:def_2; now__::_thesis:_(_(_(_i2_=_i1_+_1_or_i1_=_i2_+_1_)_&_j1_=_j2_&_(_Int_(cell_((GoB_f),i1,j1))_c=_(LeftComp_f)_\/_(RightComp_f)_implies_Int_(cell_((GoB_f),i2,j2))_c=_(LeftComp_f)_\/_(RightComp_f)_)_&_(_Int_(cell_((GoB_f),i2,j2))_c=_(LeftComp_f)_\/_(RightComp_f)_implies_Int_(cell_((GoB_f),i1,j1))_c=_(LeftComp_f)_\/_(RightComp_f)_)_)_or_(_i1_=_i2_&_(_j2_=_j1_+_1_or_j1_=_j2_+_1_)_&_(_Int_(cell_((GoB_f),i1,j1))_c=_(LeftComp_f)_\/_(RightComp_f)_implies_Int_(cell_((GoB_f),i2,j2))_c=_(LeftComp_f)_\/_(RightComp_f)_)_&_(_Int_(cell_((GoB_f),i2,j2))_c=_(LeftComp_f)_\/_(RightComp_f)_implies_Int_(cell_((GoB_f),i1,j1))_c=_(LeftComp_f)_\/_(RightComp_f)_)_)_) percases ( ( ( i2 = i1 + 1 or i1 = i2 + 1 ) & j1 = j2 ) or ( i1 = i2 & ( j2 = j1 + 1 or j1 = j2 + 1 ) ) ) by A5, GOBRD10:def_1; case ( ( i2 = i1 + 1 or i1 = i2 + 1 ) & j1 = j2 ) ; ::_thesis: ( Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) iff Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) ) hence ( Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) iff Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) ) by A1, A2, Lm5; ::_thesis: verum end; case ( i1 = i2 & ( j2 = j1 + 1 or j1 = j2 + 1 ) ) ; ::_thesis: ( Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) iff Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) ) hence ( Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) iff Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) ) by A1, A3, Lm6; ::_thesis: verum end; end; end; hence ( Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) iff Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) ) ; ::_thesis: verum end; theorem Th7: :: GOBRD12:7 for f being non constant standard special_circular_sequence for F1, F2 being FinSequence of NAT st len F1 = len F2 & ex i being Element of NAT st ( i in dom F1 & Int (cell ((GoB f),(F1 /. i),(F2 /. i))) c= (LeftComp f) \/ (RightComp f) ) & ( for i, k1, k2 being Element of NAT st i in dom F1 & k1 = F1 . i & k2 = F2 . i holds ( k1 <= len (GoB f) & k2 <= width (GoB f) ) ) holds for i being Element of NAT st i in dom F1 holds Int (cell ((GoB f),(F1 /. i),(F2 /. i))) c= (LeftComp f) \/ (RightComp f) proof let f be non constant standard special_circular_sequence; ::_thesis: for F1, F2 being FinSequence of NAT st len F1 = len F2 & ex i being Element of NAT st ( i in dom F1 & Int (cell ((GoB f),(F1 /. i),(F2 /. i))) c= (LeftComp f) \/ (RightComp f) ) & ( for i, k1, k2 being Element of NAT st i in dom F1 & k1 = F1 . i & k2 = F2 . i holds ( k1 <= len (GoB f) & k2 <= width (GoB f) ) ) holds for i being Element of NAT st i in dom F1 holds Int (cell ((GoB f),(F1 /. i),(F2 /. i))) c= (LeftComp f) \/ (RightComp f) let F1, F2 be FinSequence of NAT ; ::_thesis: ( len F1 = len F2 & ex i being Element of NAT st ( i in dom F1 & Int (cell ((GoB f),(F1 /. i),(F2 /. i))) c= (LeftComp f) \/ (RightComp f) ) & ( for i, k1, k2 being Element of NAT st i in dom F1 & k1 = F1 . i & k2 = F2 . i holds ( k1 <= len (GoB f) & k2 <= width (GoB f) ) ) implies for i being Element of NAT st i in dom F1 holds Int (cell ((GoB f),(F1 /. i),(F2 /. i))) c= (LeftComp f) \/ (RightComp f) ) assume that A1: len F1 = len F2 and A2: ex i being Element of NAT st ( i in dom F1 & Int (cell ((GoB f),(F1 /. i),(F2 /. i))) c= (LeftComp f) \/ (RightComp f) ) and A3: for i, k1, k2 being Element of NAT st i in dom F1 & k1 = F1 . i & k2 = F2 . i holds ( k1 <= len (GoB f) & k2 <= width (GoB f) ) ; ::_thesis: for i being Element of NAT st i in dom F1 holds Int (cell ((GoB f),(F1 /. i),(F2 /. i))) c= (LeftComp f) \/ (RightComp f) consider i1 being Element of NAT such that A4: i1 in dom F1 and A5: Int (cell ((GoB f),(F1 /. i1),(F2 /. i1))) c= (LeftComp f) \/ (RightComp f) by A2; reconsider kw1 = F1 /. i1, kw2 = F2 /. i1 as Element of NAT ; reconsider k1 = kw1 + 1, k2 = kw2 + 1 as Element of NAT ; dom F1 = Seg (len F1) by FINSEQ_1:def_3; then dom F1 = dom F2 by A1, FINSEQ_1:def_3; then A6: F2 /. i1 = F2 . i1 by A4, PARTFUN1:def_6; A7: F1 /. i1 = F1 . i1 by A4, PARTFUN1:def_6; then kw1 <= len (GoB f) by A3, A4, A6; then A8: k1 <= (len (GoB f)) + 1 by XREAL_1:6; kw2 <= width (GoB f) by A3, A4, A7, A6; then A9: k2 <= (width (GoB f)) + 1 by XREAL_1:6; A10: ( k1 -' 1 = F1 /. i1 & k2 -' 1 = F2 /. i1 ) by NAT_D:34; set n = len (GoB f); set m = width (GoB f); defpred S1[ Nat, Nat, set ] means $3 = Int (cell ((GoB f),($1 -' 1),($2 -' 1))); reconsider F = (LeftComp f) \/ (RightComp f) as Subset of (REAL 2) by EUCLID:22; A11: for i, j being Nat st [i,j] in [:(Seg ((len (GoB f)) + 1)),(Seg ((width (GoB f)) + 1)):] holds ex x being Subset of (REAL 2) st S1[i,j,x] by Lm2; ex Mm being Matrix of (len (GoB f)) + 1,(width (GoB f)) + 1, bool (REAL 2) st for i, j being Nat st [i,j] in Indices Mm holds S1[i,j,Mm * (i,j)] from MATRIX_1:sch_2(A11); then consider Mm being Matrix of (len (GoB f)) + 1,(width (GoB f)) + 1, bool (REAL 2) such that A12: for i, j being Nat st [i,j] in Indices Mm holds Mm * (i,j) = Int (cell ((GoB f),(i -' 1),(j -' 1))) ; A13: len Mm = (len (GoB f)) + 1 by MATRIX_1:def_2; then A14: dom Mm = Seg ((len (GoB f)) + 1) by FINSEQ_1:def_3; A15: len Mm > 0 by A13; A16: Seg ((width (GoB f)) + 1) = Seg (width Mm) by A13, MATRIX_1:20, A15; A17: (width (GoB f)) + 1 = width Mm by A13, MATRIX_1:20, A15; A18: for i1, j1, i2, j2 being Element of NAT st i1 in Seg ((len (GoB f)) + 1) & i2 in Seg ((len (GoB f)) + 1) & j1 in Seg ((width (GoB f)) + 1) & j2 in Seg ((width (GoB f)) + 1) & i1,j1,i2,j2 are_adjacent2 holds ( Mm * (i1,j1) c= (LeftComp f) \/ (RightComp f) iff Mm * (i2,j2) c= (LeftComp f) \/ (RightComp f) ) proof let i1, j1, i2, j2 be Element of NAT ; ::_thesis: ( i1 in Seg ((len (GoB f)) + 1) & i2 in Seg ((len (GoB f)) + 1) & j1 in Seg ((width (GoB f)) + 1) & j2 in Seg ((width (GoB f)) + 1) & i1,j1,i2,j2 are_adjacent2 implies ( Mm * (i1,j1) c= (LeftComp f) \/ (RightComp f) iff Mm * (i2,j2) c= (LeftComp f) \/ (RightComp f) ) ) assume that A19: i1 in Seg ((len (GoB f)) + 1) and A20: i2 in Seg ((len (GoB f)) + 1) and A21: j1 in Seg ((width (GoB f)) + 1) and A22: j2 in Seg ((width (GoB f)) + 1) and A23: i1,j1,i2,j2 are_adjacent2 ; ::_thesis: ( Mm * (i1,j1) c= (LeftComp f) \/ (RightComp f) iff Mm * (i2,j2) c= (LeftComp f) \/ (RightComp f) ) A24: 1 <= i2 by A20, FINSEQ_1:1; then 0 <= i2 - 1 by XREAL_1:48; then A25: i2 -' 1 = i2 - 1 by XREAL_0:def_2; [i2,j2] in [:(dom Mm),(Seg (width Mm)):] by A14, A16, A20, A22, ZFMISC_1:87; then [i2,j2] in Indices Mm by MATRIX_1:def_4; then A26: Mm * (i2,j2) = Int (cell ((GoB f),(i2 -' 1),(j2 -' 1))) by A12; reconsider ii1 = i1 -' 1, ii2 = i2 -' 1, jj1 = j1 -' 1, jj2 = j2 -' 1 as Element of NAT ; A27: 1 <= i1 by A19, FINSEQ_1:1; then 0 <= i1 - 1 by XREAL_1:48; then A28: i1 -' 1 = i1 - 1 by XREAL_0:def_2; [i1,j1] in [:(dom Mm),(Seg (width Mm)):] by A14, A17, A19, A21, ZFMISC_1:87; then [i1,j1] in Indices Mm by MATRIX_1:def_4; then A29: Mm * (i1,j1) = Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) by A12; A30: 1 <= j2 by A22, FINSEQ_1:1; then 0 <= j2 - 1 by XREAL_1:48; then A31: j2 -' 1 = j2 - 1 by XREAL_0:def_2; i2 <= (len (GoB f)) + 1 by A20, FINSEQ_1:1; then A32: i2 -' 1 <= ((len (GoB f)) + 1) - 1 by A25, XREAL_1:9; A33: 1 <= j1 by A21, FINSEQ_1:1; then 0 <= j1 - 1 by XREAL_1:48; then A34: j1 -' 1 = j1 - 1 by XREAL_0:def_2; j2 <= (width (GoB f)) + 1 by A22, FINSEQ_1:1; then A35: j2 -' 1 <= ((width (GoB f)) + 1) - 1 by A31, XREAL_1:9; j1 <= (width (GoB f)) + 1 by A21, FINSEQ_1:1; then A36: j1 -' 1 <= ((width (GoB f)) + 1) - 1 by A34, XREAL_1:9; i1 <= (len (GoB f)) + 1 by A19, FINSEQ_1:1; then A37: i1 -' 1 <= ((len (GoB f)) + 1) - 1 by A28, XREAL_1:9; ii1,jj1,ii2,jj2 are_adjacent2 by A23, A27, A24, A33, A30, GOBRD10:4; hence ( Mm * (i1,j1) c= (LeftComp f) \/ (RightComp f) iff Mm * (i2,j2) c= (LeftComp f) \/ (RightComp f) ) by A37, A32, A36, A35, A29, A26, Th6; ::_thesis: verum end; 0 + 1 <= k2 by NAT_1:13; then A38: k2 in Seg ((width (GoB f)) + 1) by A9, FINSEQ_1:1; 0 + 1 <= k1 by NAT_1:13; then A39: k1 in Seg ((len (GoB f)) + 1) by A8, FINSEQ_1:1; then [k1,k2] in [:(dom Mm),(Seg (width Mm)):] by A38, A14, A16, ZFMISC_1:87; then [k1,k2] in Indices Mm by MATRIX_1:def_4; then Mm * (k1,k2) c= (LeftComp f) \/ (RightComp f) by A5, A12, A10; then A40: for i, j being Element of NAT st i in Seg ((len (GoB f)) + 1) & j in Seg ((width (GoB f)) + 1) holds Mm * (i,j) c= F by A39, A38, A18, GOBRD10:8; thus for i being Element of NAT st i in dom F1 holds Int (cell ((GoB f),(F1 /. i),(F2 /. i))) c= (LeftComp f) \/ (RightComp f) ::_thesis: verum proof let i be Element of NAT ; ::_thesis: ( i in dom F1 implies Int (cell ((GoB f),(F1 /. i),(F2 /. i))) c= (LeftComp f) \/ (RightComp f) ) assume A41: i in dom F1 ; ::_thesis: Int (cell ((GoB f),(F1 /. i),(F2 /. i))) c= (LeftComp f) \/ (RightComp f) reconsider kx1 = F1 /. i, kx2 = F2 /. i as Element of NAT ; reconsider kk1 = kx1 + 1, kk2 = kx2 + 1 as Element of NAT ; dom F1 = Seg (len F1) by FINSEQ_1:def_3; then dom F1 = dom F2 by A1, FINSEQ_1:def_3; then A42: F2 /. i = F2 . i by A41, PARTFUN1:def_6; A43: F1 /. i = F1 . i by A41, PARTFUN1:def_6; then kx1 <= len (GoB f) by A3, A41, A42; then A44: kk1 <= (len (GoB f)) + 1 by XREAL_1:6; kx2 <= width (GoB f) by A3, A41, A43, A42; then A45: kk2 <= (width (GoB f)) + 1 by XREAL_1:6; 0 + 1 <= kk2 by NAT_1:13; then A46: kk2 in Seg ((width (GoB f)) + 1) by A45, FINSEQ_1:1; 0 + 1 <= kk1 by NAT_1:13; then A47: kk1 in Seg ((len (GoB f)) + 1) by A44, FINSEQ_1:1; A48: len Mm = (len (GoB f)) + 1 by MATRIX_1:def_2; then len Mm > 0 ; then ( dom Mm = Seg ((len (GoB f)) + 1) & Seg ((width (GoB f)) + 1) = Seg (width Mm) ) by FINSEQ_1:def_3, MATRIX_1:20, A48; then [kk1,kk2] in [:(dom Mm),(Seg (width Mm)):] by A47, A46, ZFMISC_1:87; then A49: [kk1,kk2] in Indices Mm by MATRIX_1:def_4; A50: ( kk1 -' 1 = F1 /. i & kk2 -' 1 = F2 /. i ) by NAT_D:34; Mm * (kk1,kk2) c= (LeftComp f) \/ (RightComp f) by A40, A47, A46; hence Int (cell ((GoB f),(F1 /. i),(F2 /. i))) c= (LeftComp f) \/ (RightComp f) by A12, A50, A49; ::_thesis: verum end; end; theorem Th8: :: GOBRD12:8 for f being non constant standard special_circular_sequence ex i, j being Element of NAT st ( i <= len (GoB f) & j <= width (GoB f) & Int (cell ((GoB f),i,j)) c= (LeftComp f) \/ (RightComp f) ) proof let f be non constant standard special_circular_sequence; ::_thesis: ex i, j being Element of NAT st ( i <= len (GoB f) & j <= width (GoB f) & Int (cell ((GoB f),i,j)) c= (LeftComp f) \/ (RightComp f) ) 1 + 1 <= len f by GOBOARD7:34, XXREAL_0:2; then A1: ( ex i, j being Element of NAT st ( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,1) ) & Int (left_cell (f,1)) c= LeftComp f ) by GOBOARD9:11, GOBOARD9:21; LeftComp f c= (LeftComp f) \/ (RightComp f) by XBOOLE_1:7; hence ex i, j being Element of NAT st ( i <= len (GoB f) & j <= width (GoB f) & Int (cell ((GoB f),i,j)) c= (LeftComp f) \/ (RightComp f) ) by A1, XBOOLE_1:1; ::_thesis: verum end; theorem Th9: :: GOBRD12:9 for f being non constant standard special_circular_sequence for i, j being Element of NAT st i <= len (GoB f) & j <= width (GoB f) holds Int (cell ((GoB f),i,j)) c= (LeftComp f) \/ (RightComp f) proof let f be non constant standard special_circular_sequence; ::_thesis: for i, j being Element of NAT st i <= len (GoB f) & j <= width (GoB f) holds Int (cell ((GoB f),i,j)) c= (LeftComp f) \/ (RightComp f) let i, j be Element of NAT ; ::_thesis: ( i <= len (GoB f) & j <= width (GoB f) implies Int (cell ((GoB f),i,j)) c= (LeftComp f) \/ (RightComp f) ) set n = len (GoB f); set m = width (GoB f); consider i2, j2 being Element of NAT such that A1: ( i2 <= len (GoB f) & j2 <= width (GoB f) ) and A2: Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) by Th8; assume ( i <= len (GoB f) & j <= width (GoB f) ) ; ::_thesis: Int (cell ((GoB f),i,j)) c= (LeftComp f) \/ (RightComp f) then consider fs1, fs2 being FinSequence of NAT such that A3: for k, k1, k2 being Element of NAT st k in dom fs1 & k1 = fs1 . k & k2 = fs2 . k holds ( k1 <= len (GoB f) & k2 <= width (GoB f) ) and A4: fs1 . 1 = i and A5: fs1 . (len fs1) = i2 and A6: fs2 . 1 = j and A7: fs2 . (len fs2) = j2 and A8: len fs1 = len fs2 and A9: len fs1 = ((((i -' i2) + (i2 -' i)) + (j -' j2)) + (j2 -' j)) + 1 and for k being Element of NAT st 1 <= k & k < len fs1 holds fs1 /. k,fs2 /. k,fs1 /. (k + 1),fs2 /. (k + 1) are_adjacent2 by A1, GOBRD10:7; A10: 1 <= 1 + ((((i -' i2) + (i2 -' i)) + (j -' j2)) + (j2 -' j)) by NAT_1:12; then A11: 1 in dom fs1 by A9, FINSEQ_3:25; then A12: fs1 /. 1 = i by A4, PARTFUN1:def_6; A13: 1 <= 1 + ((((i -' i2) + (i2 -' i)) + (j -' j2)) + (j2 -' j)) by NAT_1:12; then len fs2 in dom fs2 by A8, A9, FINSEQ_3:25; then A14: j2 = fs2 /. (len fs1) by A7, A8, PARTFUN1:def_6; 1 in dom fs2 by A8, A9, A10, FINSEQ_3:25; then A15: fs2 /. 1 = j by A6, PARTFUN1:def_6; A16: len fs1 in dom fs1 by A9, A13, FINSEQ_3:25; then i2 = fs1 /. (len fs1) by A5, PARTFUN1:def_6; hence Int (cell ((GoB f),i,j)) c= (LeftComp f) \/ (RightComp f) by A2, A3, A8, A16, A14, A11, A12, A15, Th7; ::_thesis: verum end; theorem :: GOBRD12:10 for f being non constant standard special_circular_sequence holds (L~ f) ` = (LeftComp f) \/ (RightComp f) proof let f be non constant standard special_circular_sequence; ::_thesis: (L~ f) ` = (LeftComp f) \/ (RightComp f) LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def_1; then consider B1 being Subset of ((TOP-REAL 2) | ((L~ f) `)) such that A1: B1 = LeftComp f and B1 is a_component by CONNSP_1:def_6; B1 c= the carrier of ((TOP-REAL 2) | ((L~ f) `)) ; then A2: LeftComp f c= (L~ f) ` by A1, Lm1; union { (Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `)))) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } c= (LeftComp f) \/ (RightComp f) proof RightComp f is_a_component_of (L~ f) ` by GOBOARD9:def_2; then consider B2 being Subset of ((TOP-REAL 2) | ((L~ f) `)) such that A3: B2 = RightComp f and A4: B2 is a_component by CONNSP_1:def_6; Cl B2 = (Cl (RightComp f)) /\ ([#] ((TOP-REAL 2) | ((L~ f) `))) by A3, PRE_TOPC:17; then A5: Cl B2 = (Cl (RightComp f)) /\ ((L~ f) `) by PRE_TOPC:def_5; reconsider B2 = B2 as Subset of ((TOP-REAL 2) | ((L~ f) `)) ; B2 is closed by A4, CONNSP_1:33; then A6: (Cl (RightComp f)) /\ ((L~ f) `) = RightComp f by A3, A5, PRE_TOPC:22; LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def_1; then consider B1 being Subset of ((TOP-REAL 2) | ((L~ f) `)) such that A7: B1 = LeftComp f and A8: B1 is a_component by CONNSP_1:def_6; Cl B1 = (Cl (LeftComp f)) /\ ([#] ((TOP-REAL 2) | ((L~ f) `))) by A7, PRE_TOPC:17; then A9: Cl B1 = (Cl (LeftComp f)) /\ ((L~ f) `) by PRE_TOPC:def_5; reconsider B1 = B1 as Subset of ((TOP-REAL 2) | ((L~ f) `)) ; B1 is closed by A8, CONNSP_1:33; then A10: ( ((Cl (LeftComp f)) \/ (Cl (RightComp f))) /\ ((L~ f) `) = ((Cl (LeftComp f)) /\ ((L~ f) `)) \/ ((Cl (RightComp f)) /\ ((L~ f) `)) & (Cl (LeftComp f)) /\ ((L~ f) `) = LeftComp f ) by A7, A9, PRE_TOPC:22, XBOOLE_1:23; reconsider Q = (L~ f) ` as Subset of (TOP-REAL 2) ; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union { (Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `)))) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } or x in (LeftComp f) \/ (RightComp f) ) A11: Cl ((LeftComp f) \/ (RightComp f)) = (Cl (LeftComp f)) \/ (Cl (RightComp f)) by PRE_TOPC:20; assume x in union { (Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `)))) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } ; ::_thesis: x in (LeftComp f) \/ (RightComp f) then consider y being set such that A12: ( x in y & y in { (Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `)))) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } ) by TARSKI:def_4; consider i, j being Element of NAT such that A13: y = Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `))) and A14: ( i <= len (GoB f) & j <= width (GoB f) ) by A12; Cl (Int (cell ((GoB f),i,j))) c= Cl ((LeftComp f) \/ (RightComp f)) by A14, Th9, PRE_TOPC:19; then A15: (Cl (Int (cell ((GoB f),i,j)))) /\ ((L~ f) `) c= ((Cl (LeftComp f)) \/ (Cl (RightComp f))) /\ ((L~ f) `) by A11, XBOOLE_1:26; reconsider P = Int (cell ((GoB f),i,j)) as Subset of (TOP-REAL 2) ; Cl (Down (P,Q)) = (Cl P) /\ Q by A14, Th1, CONNSP_3:29; hence x in (LeftComp f) \/ (RightComp f) by A12, A13, A15, A10, A6; ::_thesis: verum end; then A16: (L~ f) ` c= (LeftComp f) \/ (RightComp f) by Th4; RightComp f is_a_component_of (L~ f) ` by GOBOARD9:def_2; then consider B1 being Subset of ((TOP-REAL 2) | ((L~ f) `)) such that A17: B1 = RightComp f and B1 is a_component by CONNSP_1:def_6; B1 c= the carrier of ((TOP-REAL 2) | ((L~ f) `)) ; then B1 c= (L~ f) ` by Lm1; then (LeftComp f) \/ (RightComp f) c= (L~ f) ` by A2, A17, XBOOLE_1:8; hence (L~ f) ` = (LeftComp f) \/ (RightComp f) by A16, XBOOLE_0:def_10; ::_thesis: verum end;