let f be non constant standard special_circular_sequence; :: thesis:
let i1, j1, i2, j2 be Nat; :: thesis:
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:

case ex k being 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:

then consider k being 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)))) ;

per cases by A12, SPPOL_1:8;

case A13: ( f /. k = (GoB f) * (i2,(j1 + 1)) & f /. (k + 1) = (GoB f) * ((i2 + 1),(j1 + 1)) ) ; :: thesis:

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_0: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; :: thesis:

end;

case A18: ( f /. k = (GoB f) * ((i2 + 1),(j1 + 1)) & f /. (k + 1) = (GoB f) * (i2,(j1 + 1)) ) ; :: thesis:

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_0: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; :: thesis:

end;

hence Int (cell ((GoB f),i2,(j1 + 1))) c= (LeftComp f) \/ (RightComp f) ; :: thesis:

end;

case A23: for k being 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:

now :: thesis:

per cases by A23;

case A24: i2 = 0 ; :: thesis:

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:

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:

per cases by A4, A8, A32, XXREAL_0:1;

case A34: ( j1 >= 1 & j1 + 1 < width (GoB f) ) ; :: thesis:

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:

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:

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:

end;

case A39: ( j1 >= 1 & j1 + 1 = width (GoB f) ) ; :: thesis:

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:

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:

end;

case A43: ( j1 = 0 & j1 + 1 < width (GoB f) ) ; :: thesis:

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:

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:

end;

case A46: ( j1 = 0 & j1 + 1 = width (GoB f) ) ; :: thesis:

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:

end;

end;

case A55: i2 = len (GoB f) ; :: thesis:

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:

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:

per cases by A4, A8, A64, XXREAL_0:1;

case A66: ( j1 >= 1 & j1 + 1 < width (GoB f) ) ; :: thesis:

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:

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:

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:

end;

case A71: ( j1 >= 1 & j1 + 1 = width (GoB f) ) ; :: thesis:

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:

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:

end;

case A75: ( j1 = 0 & j1 + 1 < width (GoB f) ) ; :: thesis:

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:

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:

end;

case ( j1 = 0 & j1 + 1 = width (GoB f) ) ; :: thesis:

hence contradiction by GOBOARD7:33; :: thesis:

end;

end;

case A85: ( i2 <> 0 & i2 <> len (GoB f) & ( for k being 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:

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 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 Nat; :: thesis:
assume A88: ( 1 <= k & k + 1 <= len f ) ; :: thesis:
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:

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 object 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:

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:

per cases by A4, A8, A108, XXREAL_0:1;

case A110: ( j1 >= 1 & j1 + 1 < width (GoB f) ) ; :: thesis:

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:

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:

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:

end;

case A117: ( j1 >= 1 & j1 + 1 = width (GoB f) ) ; :: thesis:

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:

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:

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:

end;

case A121: ( j1 = 0 & j1 + 1 < width (GoB f) ) ; :: thesis:

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:

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:

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:

end;

case ( j1 = 0 & j1 + 1 = width (GoB f) ) ; :: thesis:

hence contradiction by GOBOARD7:33; :: thesis:

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;
hence Int (cell ((GoB f),i2,(j1 + 1))) c= (LeftComp f) \/ (RightComp f) by A95, A97; :: thesis:

end;

hence Int (cell ((GoB f),i2,(j1 + 1))) c= (LeftComp f) \/ (RightComp f) ; :: thesis:

end;

hence Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) by A8; :: thesis:

end;

case A126: j1 = j2 + 1 ; :: thesis:

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:

per cases ;

case ex k being 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:

then consider k being 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:

per cases by A137, SPPOL_1:8;

case A138: ( f /. k = (GoB f) * (i2,((j1 -' 1) + 1)) & f /. (k + 1) = (GoB f) * ((i2 + 1),((j1 -' 1) + 1)) ) ; :: thesis:

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_0: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; :: thesis:

end;

case A143: ( f /. k = (GoB f) * ((i2 + 1),((j1 -' 1) + 1)) & f /. (k + 1) = (GoB f) * (i2,((j1 -' 1) + 1)) ) ; :: thesis:

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_0: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; :: thesis:

end;

hence Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) by A126, NAT_D:34; :: thesis:

end;

case A148: for k being 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:

now :: thesis:

per cases by A148;

case A149: i2 = 0 ; :: thesis:

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:

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:

per cases by A2, A126, XXREAL_0:1;

case A158: ( j2 + 1 < width (GoB f) & j2 > 0 ) ; :: thesis:

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:

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:

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:

end;

case A164: ( j2 + 1 < width (GoB f) & j2 = 0 ) ; :: thesis:

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:

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:

end;

case A168: ( j2 + 1 = width (GoB f) & j2 > 0 ) ; :: thesis:

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:

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:

end;

case A172: ( j2 + 1 = width (GoB f) & j2 = 0 ) ; :: thesis:

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:

end;

end;

case A181: i2 = len (GoB f) ; :: thesis:

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:

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:

per cases by A2, A126, XXREAL_0:1;

case A190: ( j2 + 1 < width (GoB f) & j2 > 0 ) ; :: thesis:

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:

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:

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:

end;

case A197: ( j2 + 1 < width (GoB f) & j2 = 0 ) ; :: thesis:

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:

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:

end;

case A200: ( j2 + 1 = width (GoB f) & j2 > 0 ) ; :: thesis:

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:

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:

end;

case ( j2 + 1 = width (GoB f) & j2 = 0 ) ; :: thesis:

hence contradiction by GOBOARD7:33; :: thesis:

end;

end;

case A210: ( i2 <> 0 & i2 <> len (GoB f) & ( for k being 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:

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 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 Nat; :: thesis:
assume A213: ( 1 <= k & k + 1 <= len f ) ; :: thesis:
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:

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 object 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:

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:

per cases by A2, A126, A233, XXREAL_0:1;

case A235: ( j2 >= 1 & j2 + 1 < width (GoB f) ) ; :: thesis:

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:

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:

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:

end;

case A241: ( j2 >= 1 & j2 + 1 = width (GoB f) ) ; :: thesis:

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:

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:

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:

end;

case A245: ( j2 = 0 & j2 + 1 < width (GoB f) ) ; :: thesis:

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:

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:

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:

end;

case ( j2 = 0 & j2 + 1 = width (GoB f) ) ; :: thesis:

hence contradiction by GOBOARD7:33; :: thesis:

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;
hence Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) by A222, A221; :: thesis:

end;

hence Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) ; :: thesis:

end;

hence Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) ; :: thesis:

end;

hence Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) ; :: thesis:

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: