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
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
per cases ( j2 = j1 + 1 or j1 = j2 + 1 ) by A5;
case A8: j2 = j1 + 1 ; :: thesis: Int (cell (GoB f),i2,j2) c= (LeftComp f) \/ (RightComp f)
now
per cases ( 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
per cases ( ( 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:25;
case A13: ( 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:24, 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:8;
then A16: ( Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] & j1 + 1 in Seg (width (GoB f)) ) by A4, A8, FINSEQ_1:3, MATRIX_1:def 5;
1 <= i2 + 1 by NAT_1:11;
then i2 + 1 in dom (GoB f) by A15, FINSEQ_3:27;
then A17: [(i2 + 1),(j1 + 1)] in Indices (GoB f) by A16, ZFMISC_1:106;
i2 >= 0 + 1 by A10, NAT_1:13;
then i2 in dom (GoB f) by A3, FINSEQ_3:27;
then [i2,(j1 + 1)] in Indices (GoB f) by A16, ZFMISC_1:106;
then left_cell f,k = cell (GoB f),i2,(j1 + 1) by A9, A13, A17, GOBOARD5:29;
hence Int (cell (GoB f),i2,(j1 + 1)) c= (LeftComp f) \/ (RightComp f) by A14, XBOOLE_1:1; :: thesis: verum
end;
case A18: ( 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:28, 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:8;
then A21: ( Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] & j1 + 1 in Seg (width (GoB f)) ) by A4, A8, FINSEQ_1:3, MATRIX_1:def 5;
1 <= i2 + 1 by NAT_1:11;
then i2 + 1 in dom (GoB f) by A20, FINSEQ_3:27;
then A22: [(i2 + 1),(j1 + 1)] in Indices (GoB f) by A21, ZFMISC_1:106;
i2 >= 0 + 1 by A10, NAT_1:13;
then i2 in dom (GoB f) by A3, FINSEQ_3:27;
then [i2,(j1 + 1)] in Indices (GoB f) by A21, ZFMISC_1:106;
then right_cell f,k = cell (GoB f),i2,(j1 + 1) by A9, A18, A22, GOBOARD5:30;
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;
case A23: 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
per cases ( 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;
case A24: 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:34;
A26: 1 < width (GoB f) by GOBOARD7:35;
reconsider P = {p} as Subset of (TOP-REAL 2) ;
A27: p `1 < (p `1 ) + 1 by XREAL_1:31;
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:3;
then A29: p `1 = (((GoB f) * 1,1) `1 ) - 1 by EUCLID:56;
p in { |[s,r]| where s, r is Real : s <= ((GoB f) * 1,1) `1 }
proof
p = |[(p `1 ),(p `2 )]| by EUCLID:57;
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:11;
( ( 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:43, TARSKI:def 1;
then reconsider p1 = p as Point of ((TOP-REAL 2) | ((L~ f) ` )) by PRE_TOPC:29;
A32: ( j1 = 0 or j1 >= 0 + 1 ) by NAT_1:13;
A33: now
per cases ( ( 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;
case A34: ( 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:5;
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:6;
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:5;
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:6;
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;
case A39: ( 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:5;
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:7;
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:6;
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;
case A43: ( 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:5;
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:6;
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:8;
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;
case A46: ( 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:7;
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:8;
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, Th3;
then A48: Cl (Down (Int (cell (GoB f),i2,(j1 + 1))),((L~ f) ` )) c= Component_of p1 by A3, A4, A8, Th4, GOBRD11:1;
Down (RightComp f),((L~ f) ` ) is closed by Lm4, CONNSP_1:35;
then A49: Cl (Down (RightComp f),((L~ f) ` )) = Down (RightComp f),((L~ f) ` ) by PRE_TOPC:52;
Down (LeftComp f),((L~ f) ` ) is closed by Lm3, CONNSP_1:35;
then A50: Cl (Down (LeftComp f),((L~ f) ` )) = Down (LeftComp f),((L~ f) ` ) by PRE_TOPC:52;
(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:50;
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, Th4, PRE_TOPC:48;
A53: ( Down (LeftComp f),((L~ f) ` ) = LeftComp f & Down (RightComp f),((L~ f) ` ) = RightComp f ) by Th6;
Down (Int (cell (GoB f),i2,j1)),((L~ f) ` ) c= (LeftComp f) \/ (RightComp f) by A1, A2, A6, A7, Th4;
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:49;
p in Cl (Down (Int (cell (GoB f),i2,j1)),((L~ f) ` )) by A2, A3, A33, Th3;
then Component_of p1 c= (Down (LeftComp f),((L~ f) ` )) \/ (Down (RightComp f),((L~ f) ` )) by A54, A51, Th6, 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;
case A55: 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:34;
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:35;
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:3;
then A60: p `1 = (((GoB f) * (len (GoB f)),1) `1 ) + 1 by EUCLID:56;
then A61: ((GoB f) * (len (GoB f)),1) `1 < p `1 by XREAL_1:31;
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:57;
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:10;
((GoB f) * (len (GoB f)),1) `1 < (((GoB f) * (len (GoB f)),1) `1 ) + 1 by XREAL_1:31;
then A63: ( p in {p} & {p} c= (L~ f) ` ) by A60, A57, SUBSET_1:43, TARSKI:def 1;
then reconsider p1 = p as Point of ((TOP-REAL 2) | ((L~ f) ` )) by PRE_TOPC:29;
A64: ( j1 = 0 or j1 >= 0 + 1 ) by NAT_1:13;
A65: now
per cases ( ( 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;
case A66: ( 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:5;
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:6;
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:5;
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:6;
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;
case A71: ( 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:5;
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:7;
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:6;
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;
case A75: ( 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:5;
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:6;
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:8;
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;
end;
end;
then p in Cl (Down (Int (cell (GoB f),i2,(j1 + 1))),((L~ f) ` )) by A3, Th3;
then A78: Cl (Down (Int (cell (GoB f),i2,(j1 + 1))),((L~ f) ` )) c= Component_of p1 by A3, A4, A8, Th4, GOBRD11:1;
Down (RightComp f),((L~ f) ` ) is closed by Lm4, CONNSP_1:35;
then A79: Cl (Down (RightComp f),((L~ f) ` )) = Down (RightComp f),((L~ f) ` ) by PRE_TOPC:52;
Down (LeftComp f),((L~ f) ` ) is closed by Lm3, CONNSP_1:35;
then A80: Cl (Down (LeftComp f),((L~ f) ` )) = Down (LeftComp f),((L~ f) ` ) by PRE_TOPC:52;
(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:50;
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, Th4, PRE_TOPC:48;
A83: ( Down (LeftComp f),((L~ f) ` ) = LeftComp f & Down (RightComp f),((L~ f) ` ) = RightComp f ) by Th6;
Down (Int (cell (GoB f),i2,j1)),((L~ f) ` ) c= (LeftComp f) \/ (RightComp f) by A1, A2, A6, A7, Th4;
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:49;
p in Cl (Down (Int (cell (GoB f),i2,j1)),((L~ f) ` )) by A2, A3, A65, Th3;
then Component_of p1 c= (Down (LeftComp f),((L~ f) ` )) \/ (Down (RightComp f),((L~ f) ` )) by A84, A81, Th6, 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;
case A85: ( 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 5;
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:42;
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:9
.= (1 / 2) * ((((GoB f) * i2,(j1 + 1)) `1 ) + (((GoB f) * (i2 + 1),(j1 + 1)) `1 )) by TOPREAL3:7 ;
reconsider P = {p} as Subset of (TOP-REAL 2) ;
A91: 1 < len (GoB f) by GOBOARD7:34;
Down (RightComp f),((L~ f) ` ) is closed by Lm4, CONNSP_1:35;
then A92: Cl (Down (RightComp f),((L~ f) ` )) = Down (RightComp f),((L~ f) ` ) by PRE_TOPC:52;
Down (LeftComp f),((L~ f) ` ) is closed by Lm3, CONNSP_1:35;
then A93: Cl (Down (LeftComp f),((L~ f) ` )) = Down (LeftComp f),((L~ f) ` ) by PRE_TOPC:52;
(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:50;
A95: ( Down (LeftComp f),((L~ f) ` ) = LeftComp f & Down (RightComp f),((L~ f) ` ) = RightComp f ) by Th6;
Down (Int (cell (GoB f),i2,j1)),((L~ f) ` ) c= (LeftComp f) \/ (RightComp f) by A1, A2, A6, A7, Th4;
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:49;
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, Th4, PRE_TOPC:48;
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:43, TARSKI:def 1;
then reconsider p1 = p as Point of ((TOP-REAL 2) | ((L~ f) ` )) by PRE_TOPC:29;
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:9
.= (1 / 2) * ((((GoB f) * i2,(j1 + 1)) `2 ) + (((GoB f) * (i2 + 1),(j1 + 1)) `2 )) by TOPREAL3:7 ;
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:57;
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:4;
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:10;
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:76;
(((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:10;
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:76;
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:57;
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:9;
A108: ( j1 = 0 or j1 >= 0 + 1 ) by NAT_1:13;
A109: now
per cases ( ( 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;
case A110: ( 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:5;
( ((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:2;
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:6;
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:5;
( ((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:2;
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:6;
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;
case A117: ( 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:5;
( ((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:2;
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:6;
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:2;
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:7;
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;
case A121: ( 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:5;
( ((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:2;
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:6;
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:2;
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:8;
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;
end;
end;
then p in Cl (Down (Int (cell (GoB f),i2,(j1 + 1))),((L~ f) ` )) by A3, Th3;
then A125: Cl (Down (Int (cell (GoB f),i2,(j1 + 1))),((L~ f) ` )) c= Component_of p1 by A3, A4, A8, Th4, GOBRD11:1;
p in Cl (Down (Int (cell (GoB f),i2,j1)),((L~ f) ` )) by A2, A3, A109, Th3;
then Component_of p1 c= (Down (LeftComp f),((L~ f) ` )) \/ (Down (RightComp f),((L~ f) ` )) by A96, A94, Th6, 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;
case A126: 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
per cases ( 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
per cases ( ( 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:25;
case A138: ( 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:28, 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:3, MATRIX_1:def 5;
1 <= i2 + 1 by NAT_1:11;
then i2 + 1 in dom (GoB f) by A140, FINSEQ_3:27;
then A142: [(i2 + 1),((j1 -' 1) + 1)] in Indices (GoB f) by A141, ZFMISC_1:106;
i2 >= 0 + 1 by A135, NAT_1:13;
then i2 in dom (GoB f) by A3, FINSEQ_3:27;
then [i2,((j1 -' 1) + 1)] in Indices (GoB f) by A141, ZFMISC_1:106;
then right_cell f,k = cell (GoB f),i2,(j1 -' 1) by A134, A138, A142, GOBOARD5:29;
hence Int (cell (GoB f),i2,(j1 -' 1)) c= (LeftComp f) \/ (RightComp f) by A139, XBOOLE_1:1; :: thesis: verum
end;
case A143: ( 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:24, 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:3, MATRIX_1:def 5;
1 <= i2 + 1 by NAT_1:11;
then i2 + 1 in dom (GoB f) by A145, FINSEQ_3:27;
then A147: [(i2 + 1),((j1 -' 1) + 1)] in Indices (GoB f) by A146, ZFMISC_1:106;
i2 >= 0 + 1 by A135, NAT_1:13;
then i2 in dom (GoB f) by A3, FINSEQ_3:27;
then [i2,((j1 -' 1) + 1)] in Indices (GoB f) by A146, ZFMISC_1:106;
then left_cell f,k = cell (GoB f),i2,(j1 -' 1) by A134, A143, A147, GOBOARD5:30;
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;
case A148: 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
per cases ( 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;
case A149: 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:34;
A151: 1 < width (GoB f) by GOBOARD7:35;
reconsider P = {p} as Subset of (TOP-REAL 2) ;
A152: p `1 < (p `1 ) + 1 by XREAL_1:31;
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:3;
then A154: p `1 = (((GoB f) * 1,1) `1 ) - 1 by EUCLID:56;
p in { |[s,r]| where s, r is Real : s <= ((GoB f) * 1,1) `1 }
proof
p = |[(p `1 ),(p `2 )]| by EUCLID:57;
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:11;
( ( 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:43, TARSKI:def 1;
then reconsider p1 = p as Point of ((TOP-REAL 2) | ((L~ f) ` )) by PRE_TOPC:29;
A157: now
per cases ( ( 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;
case A158: ( 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:5;
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:5;
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:6;
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:6;
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;
case A164: ( 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:5;
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:6;
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:8;
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;
case A168: ( 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:5;
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:7;
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:6;
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;
case A172: ( 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:7;
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:8;
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, Th3;
then A174: Cl (Down (Int (cell (GoB f),i2,j2)),((L~ f) ` )) c= Component_of p1 by A3, A4, Th4, GOBRD11:1;
Down (RightComp f),((L~ f) ` ) is closed by Lm4, CONNSP_1:35;
then A175: Cl (Down (RightComp f),((L~ f) ` )) = Down (RightComp f),((L~ f) ` ) by PRE_TOPC:52;
Down (LeftComp f),((L~ f) ` ) is closed by Lm3, CONNSP_1:35;
then A176: Cl (Down (LeftComp f),((L~ f) ` )) = Down (LeftComp f),((L~ f) ` ) by PRE_TOPC:52;
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, Th4, PRE_TOPC:48;
(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:50;
A179: ( Down (LeftComp f),((L~ f) ` ) = LeftComp f & Down (RightComp f),((L~ f) ` ) = RightComp f ) by Th6;
Down (Int (cell (GoB f),i2,j1)),((L~ f) ` ) c= (LeftComp f) \/ (RightComp f) by A1, A2, A6, A7, Th4;
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:49;
p in Cl (Down (Int (cell (GoB f),i2,(j2 + 1))),((L~ f) ` )) by A3, A157, Th3;
then Component_of p1 c= (Down (LeftComp f),((L~ f) ` )) \/ (Down (RightComp f),((L~ f) ` )) by A126, A180, A178, Th6, 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;
case A181: 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:34;
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:35;
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:3;
then A185: p `1 = (((GoB f) * (len (GoB f)),1) `1 ) + 1 by EUCLID:56;
then A186: ((GoB f) * (len (GoB f)),1) `1 < p `1 by XREAL_1:31;
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:57;
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:10;
((GoB f) * (len (GoB f)),1) `1 < (((GoB f) * (len (GoB f)),1) `1 ) + 1 by XREAL_1:31;
then A188: ( p in {p} & {p} c= (L~ f) ` ) by A185, A183, SUBSET_1:43, TARSKI:def 1;
then reconsider p1 = p as Point of ((TOP-REAL 2) | ((L~ f) ` )) by PRE_TOPC:29;
A189: now
per cases ( ( 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;
case A190: ( 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:5;
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:6;
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:5;
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:6;
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;
case A197: ( 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:5;
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:6;
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:8;
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;
case A200: ( 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:5;
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:6;
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:7;
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;
end;
end;
then p in Cl (Down (Int (cell (GoB f),i2,j2)),((L~ f) ` )) by A3, A4, Th3;
then A203: Cl (Down (Int (cell (GoB f),i2,j2)),((L~ f) ` )) c= Component_of p1 by A3, A4, Th4, GOBRD11:1;
Down (RightComp f),((L~ f) ` ) is closed by Lm4, CONNSP_1:35;
then A204: Cl (Down (RightComp f),((L~ f) ` )) = Down (RightComp f),((L~ f) ` ) by PRE_TOPC:52;
Down (LeftComp f),((L~ f) ` ) is closed by Lm3, CONNSP_1:35;
then A205: Cl (Down (LeftComp f),((L~ f) ` )) = Down (LeftComp f),((L~ f) ` ) by PRE_TOPC:52;
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, Th4, PRE_TOPC:48;
(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:50;
A208: ( Down (LeftComp f),((L~ f) ` ) = LeftComp f & Down (RightComp f),((L~ f) ` ) = RightComp f ) by Th6;
Down (Int (cell (GoB f),i2,j1)),((L~ f) ` ) c= (LeftComp f) \/ (RightComp f) by A1, A2, A6, A7, Th4;
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:49;
p in Cl (Down (Int (cell (GoB f),i2,(j2 + 1))),((L~ f) ` )) by A3, A189, Th3;
then Component_of p1 c= (Down (LeftComp f),((L~ f) ` )) \/ (Down (RightComp f),((L~ f) ` )) by A126, A209, A207, Th6, 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;
case A210: ( 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 5;
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:42;
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:9
.= (1 / 2) * ((((GoB f) * i2,(j2 + 1)) `1 ) + (((GoB f) * (i2 + 1),(j2 + 1)) `1 )) by TOPREAL3:7 ;
reconsider P = {p} as Subset of (TOP-REAL 2) ;
A216: 1 < len (GoB f) by GOBOARD7:34;
Down (RightComp f),((L~ f) ` ) is closed by Lm4, CONNSP_1:35;
then A217: Cl (Down (RightComp f),((L~ f) ` )) = Down (RightComp f),((L~ f) ` ) by PRE_TOPC:52;
Down (LeftComp f),((L~ f) ` ) is closed by Lm3, CONNSP_1:35;
then A218: Cl (Down (LeftComp f),((L~ f) ` )) = Down (LeftComp f),((L~ f) ` ) by PRE_TOPC:52;
(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:50;
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, Th4, PRE_TOPC:48;
A222: ( Down (LeftComp f),((L~ f) ` ) = LeftComp f & Down (RightComp f),((L~ f) ` ) = RightComp f ) by Th6;
Down (Int (cell (GoB f),i2,j1)),((L~ f) ` ) c= (LeftComp f) \/ (RightComp f) by A1, A2, A6, A7, Th4;
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:49;
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:43, TARSKI:def 1;
then reconsider p1 = p as Point of ((TOP-REAL 2) | ((L~ f) ` )) by PRE_TOPC:29;
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:4;
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:10;
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:76;
(((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:10;
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:76;
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:57;
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:9;
p `2 = (1 / 2) * ((((GoB f) * i2,(j2 + 1)) + ((GoB f) * (i2 + 1),(j2 + 1))) `2 ) by TOPREAL3:9
.= (1 / 2) * ((((GoB f) * i2,(j2 + 1)) `2 ) + (((GoB f) * (i2 + 1),(j2 + 1)) `2 )) by TOPREAL3:7 ;
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:57;
A233: ( j2 = 0 or j2 >= 0 + 1 ) by NAT_1:13;
A234: now
per cases ( ( 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;
case A235: ( 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:5;
( ((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:2;
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:6;
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:5;
( ((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:2;
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:6;
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;
case A241: ( 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:5;
( ((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:2;
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:6;
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:2;
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:7;
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;
case A245: ( 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:5;
( ((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:2;
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:6;
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:2;
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:8;
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;
end;
end;
then p in Cl (Down (Int (cell (GoB f),i2,j2)),((L~ f) ` )) by A3, A4, Th3;
then A249: Cl (Down (Int (cell (GoB f),i2,j2)),((L~ f) ` )) c= Component_of p1 by A3, A4, Th4, GOBRD11:1;
p in Cl (Down (Int (cell (GoB f),i2,j1)),((L~ f) ` )) by A3, A126, A234, Th3;
then Component_of p1 c= (Down (LeftComp f),((L~ f) ` )) \/ (Down (RightComp f),((L~ f) ` )) by A223, A219, Th6, 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