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: ( i2 = i1 + 1 or i1 = i2 + 1 ) and
A6: j1 = j2 ; :: thesis:

case ex k being Nat st
( 1 <= k & k + 1 <= len f & j2 <> 0 & j2 <> width (GoB f) & LSeg ((f /. k),(f /. (k + 1))) = LSeg (((GoB f) * ((i1 + 1),j2)),((GoB f) * ((i1 + 1),(j2 + 1)))) ) ; :: thesis:

then consider k being Nat such that
A9: ( 1 <= k & k + 1 <= len f ) and
A10: j2 <> 0 and
A11: j2 <> width (GoB f) and
A12: LSeg ((f /. k),(f /. (k + 1))) = LSeg (((GoB f) * ((i1 + 1),j2)),((GoB f) * ((i1 + 1),(j2 + 1)))) ;

per cases by A12, SPPOL_1:8;

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

A14: ( Int (right_cell (f,k)) c= RightComp f & RightComp f c= (LeftComp f) \/ (RightComp f) ) by A9, GOBOARD9:25, XBOOLE_1:7;
j2 < width (GoB f) by A4, A11, XXREAL_0:1;
then A15: j2 + 1 <= width (GoB f) by NAT_1:13;
0 + 1 <= i1 + 1 by XREAL_1:6;
then A16: ( Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] & i1 + 1 in dom (GoB f) ) by A3, A8, FINSEQ_3:25, MATRIX_0:def 4;
1 <= j2 + 1 by NAT_1:11;
then j2 + 1 in Seg (width (GoB f)) by A15, FINSEQ_1:1;
then A17: [(i1 + 1),(j2 + 1)] in Indices (GoB f) by A16, ZFMISC_1:87;
j2 >= 0 + 1 by A10, NAT_1:13;
then j2 in Seg (width (GoB f)) by A4, FINSEQ_1:1;
then [(i1 + 1),j2] in Indices (GoB f) by A16, ZFMISC_1:87;
then right_cell (f,k) = cell ((GoB f),(i1 + 1),j2) by A9, A13, A17, GOBOARD5:27;
hence Int (cell ((GoB f),(i1 + 1),j2)) c= (LeftComp f) \/ (RightComp f) by A14; :: thesis:

end;

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

A19: ( Int (left_cell (f,k)) c= LeftComp f & LeftComp f c= (LeftComp f) \/ (RightComp f) ) by A9, GOBOARD9:21, XBOOLE_1:7;
j2 < width (GoB f) by A4, A11, XXREAL_0:1;
then A20: j2 + 1 <= width (GoB f) by NAT_1:13;
0 + 1 <= i1 + 1 by XREAL_1:6;
then A21: ( Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] & i1 + 1 in dom (GoB f) ) by A3, A8, FINSEQ_3:25, MATRIX_0:def 4;
1 <= j2 + 1 by NAT_1:11;
then j2 + 1 in Seg (width (GoB f)) by A20, FINSEQ_1:1;
then A22: [(i1 + 1),(j2 + 1)] in Indices (GoB f) by A21, ZFMISC_1:87;
j2 >= 0 + 1 by A10, NAT_1:13;
then j2 in Seg (width (GoB f)) by A4, FINSEQ_1:1;
then [(i1 + 1),j2] in Indices (GoB f) by A21, ZFMISC_1:87;
then left_cell (f,k) = cell ((GoB f),(i1 + 1),j2) by A9, A18, A22, GOBOARD5:30;
hence Int (cell ((GoB f),(i1 + 1),j2)) c= (LeftComp f) \/ (RightComp f) by A19; :: thesis:

end;

hence Int (cell ((GoB f),(i1 + 1),j2)) 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 j2 <> 0 or not j2 <> width (GoB f) or not LSeg ((f /. k),(f /. (k + 1))) = LSeg (((GoB f) * ((i1 + 1),j2)),((GoB f) * ((i1 + 1),(j2 + 1)))) ) ; :: thesis:

now :: thesis:

per cases by A23;

case A24: j2 = 0 ; :: thesis:

reconsider p = |[(((GoB f) * ((i1 + 1),1)) `1),((((GoB f) * ((i1 + 1),1)) `2) - 1)]| as Point of (TOP-REAL 2) ;
A25: 1 < width (GoB f) by GOBOARD7:33;
A26: 1 < len (GoB f) by GOBOARD7:32;
reconsider P = {p} as Subset of (TOP-REAL 2) ;
A27: p `2 < (p `2) + 1 by XREAL_1:29;
A28: 1 <= i1 + 1 by NAT_1:11;
then ((GoB f) * ((i1 + 1),1)) `2 = ((GoB f) * (1,1)) `2 by A3, A8, A25, GOBOARD5:1;
then A29: p `2 = (((GoB f) * (1,1)) `2) - 1 by EUCLID:52;
p in { |[r,s]| where r, s is Real : s <= ((GoB f) * (1,1)) `2 }

proof

p = |[(p `1),(p `2)]| by EUCLID:53;
hence p in { |[r,s]| where r, s is Real : s <= ((GoB f) * (1,1)) `2 } by A29, A27; :: thesis:

end;

then A30: p in h_strip ((GoB f),j2) by A24, A26, GOBOARD5:7;
( ( for q being Point of (TOP-REAL 2) st q in P holds
q `2 < ((GoB f) * (1,1)) `2 ) implies P misses L~ f ) by GOBOARD8:23;
then A31: ( p in {p} & {p} c= (L~ f) ` ) by A29, A27, SUBSET_1:23, TARSKI:def 1;
then reconsider p1 = p as Point of ((TOP-REAL 2) | ((L~ f) `)) by PRE_TOPC:8;
A32: ( i1 = 0 or i1 >= 0 + 1 ) by NAT_1:13;

A33: now :: thesis:

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

case A34: ( i1 >= 1 & i1 + 1 < len (GoB f) ) ; :: thesis:

then A35: (i1 + 1) + 1 <= len (GoB f) by NAT_1:13;
A36: p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i1 + 1),1)) `1 <= r & r <= ((GoB f) * (((i1 + 1) + 1),1)) `1 ) }

proof

i1 + 1 < (i1 + 1) + 1 by NAT_1:13;
then ((GoB f) * ((i1 + 1),1)) `1 <= ((GoB f) * (((i1 + 1) + 1),1)) `1 by A25, A28, A35, GOBOARD5:3;
hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i1 + 1),1)) `1 <= r & r <= ((GoB f) * (((i1 + 1) + 1),1)) `1 ) } ; :: thesis:

end;

1 <= i1 + 1 by NAT_1:11;
then p in v_strip ((GoB f),(i1 + 1)) by A25, A34, A36, GOBOARD5:8;
then p in (v_strip ((GoB f),(i1 + 1))) /\ (h_strip ((GoB f),j2)) by A30, XBOOLE_0:def 4;
then A37: p in cell ((GoB f),(i1 + 1),j2) by GOBOARD5:def 3;
A38: p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i1,1)) `1 <= r & r <= ((GoB f) * ((i1 + 1),1)) `1 ) }

proof

i1 < i1 + 1 by NAT_1:13;
then ((GoB f) * (i1,1)) `1 < ((GoB f) * ((i1 + 1),1)) `1 by A25, A34, GOBOARD5:3;
hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i1,1)) `1 <= r & r <= ((GoB f) * ((i1 + 1),1)) `1 ) } ; :: thesis:

end;

i1 < len (GoB f) by A34, NAT_1:13;
then p in v_strip ((GoB f),i1) by A25, A34, A38, GOBOARD5:8;
then p in (v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j2)) by A30, XBOOLE_0:def 4;
then p in cell ((GoB f),i1,j2) by GOBOARD5:def 3;
hence ( p in (cell ((GoB f),(i1 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i1,j2)) /\ ((L~ f) `) ) by A31, A37, XBOOLE_0:def 4; :: thesis:

end;

case A39: ( i1 >= 1 & i1 + 1 = len (GoB f) ) ; :: thesis:

A40: i1 < i1 + 1 by NAT_1:13;
A41: p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i1,1)) `1 <= r & r <= ((GoB f) * ((i1 + 1),1)) `1 ) }

proof

((GoB f) * (i1,1)) `1 < ((GoB f) * ((i1 + 1),1)) `1 by A25, A39, A40, GOBOARD5:3;
hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i1,1)) `1 <= r & r <= ((GoB f) * ((i1 + 1),1)) `1 ) } ; :: thesis:

end;

p in { |[r,s]| where r, s is Real : ((GoB f) * ((i1 + 1),1)) `1 <= r } ;
then p in v_strip ((GoB f),(i1 + 1)) by A25, A39, GOBOARD5:9;
then p in (v_strip ((GoB f),(i1 + 1))) /\ (h_strip ((GoB f),j2)) by A30, XBOOLE_0:def 4;
then A42: p in cell ((GoB f),(i1 + 1),j2) by GOBOARD5:def 3;
i1 < len (GoB f) by A39, NAT_1:13;
then p in v_strip ((GoB f),i1) by A25, A39, A41, GOBOARD5:8;
then p in (v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j2)) by A30, XBOOLE_0:def 4;
then p in cell ((GoB f),i1,j2) by GOBOARD5:def 3;
hence ( p in (cell ((GoB f),(i1 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i1,j2)) /\ ((L~ f) `) ) by A31, A42, XBOOLE_0:def 4; :: thesis:

end;

case A43: ( i1 = 0 & i1 + 1 < len (GoB f) ) ; :: thesis:

then A44: (i1 + 1) + 1 <= len (GoB f) by NAT_1:13;
p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i1 + 1),1)) `1 <= r & r <= ((GoB f) * (((i1 + 1) + 1),1)) `1 ) }

proof

i1 + 1 < (i1 + 1) + 1 by NAT_1:13;
then ((GoB f) * ((i1 + 1),1)) `1 <= ((GoB f) * (((i1 + 1) + 1),1)) `1 by A25, A28, A44, GOBOARD5:3;
hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i1 + 1),1)) `1 <= r & r <= ((GoB f) * (((i1 + 1) + 1),1)) `1 ) } ; :: thesis:

end;

then p in v_strip ((GoB f),(i1 + 1)) by A25, A43, GOBOARD5:8;
then p in (v_strip ((GoB f),(i1 + 1))) /\ (h_strip ((GoB f),j2)) by A30, XBOOLE_0:def 4;
then A45: p in cell ((GoB f),(i1 + 1),j2) by GOBOARD5:def 3;
p in { |[r,s]| where r, s is Real : r <= ((GoB f) * (1,1)) `1 } by A43;
then p in v_strip ((GoB f),i1) by A25, A43, GOBOARD5:10;
then p in (v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j2)) by A30, XBOOLE_0:def 4;
then p in cell ((GoB f),i1,j2) by GOBOARD5:def 3;
hence ( p in (cell ((GoB f),(i1 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i1,j2)) /\ ((L~ f) `) ) by A31, A45, XBOOLE_0:def 4; :: thesis:

end;

case A46: ( i1 = 0 & i1 + 1 = len (GoB f) ) ; :: thesis:

p in { |[r,s]| where r, s is Real : ((GoB f) * ((i1 + 1),1)) `1 <= r } ;
then p in v_strip ((GoB f),(i1 + 1)) by A25, A46, GOBOARD5:9;
then p in (v_strip ((GoB f),(i1 + 1))) /\ (h_strip ((GoB f),j2)) by A30, XBOOLE_0:def 4;
then A47: p in cell ((GoB f),(i1 + 1),j2) by GOBOARD5:def 3;
p in { |[r,s]| where r, s is Real : r <= ((GoB f) * (1,1)) `1 } by A46;
then p in v_strip ((GoB f),i1) by A25, A46, GOBOARD5:10;
then p in (v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j2)) by A30, XBOOLE_0:def 4;
then p in cell ((GoB f),i1,j2) by GOBOARD5:def 3;
hence ( p in (cell ((GoB f),(i1 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i1,j2)) /\ ((L~ f) `) ) by A31, A47, XBOOLE_0:def 4; :: thesis:

end;

end;

case A55: j2 = width (GoB f) ; :: thesis:

reconsider p = |[(((GoB f) * ((i1 + 1),(width (GoB f)))) `1),((((GoB f) * ((i1 + 1),(width (GoB f)))) `2) + 1)]| as Point of (TOP-REAL 2) ;
A56: 1 < width (GoB f) by GOBOARD7:33;
reconsider P = {p} as Subset of (TOP-REAL 2) ;
A57: ( ( for q being Point of (TOP-REAL 2) st q in P holds
((GoB f) * (1,(width (GoB f)))) `2 < q `2 ) implies P misses L~ f ) by GOBOARD8:24;
A58: 1 < len (GoB f) by GOBOARD7:32;
A59: 1 <= 1 + i1 by NAT_1:11;
then ((GoB f) * ((i1 + 1),(width (GoB f)))) `2 = ((GoB f) * (1,(width (GoB f)))) `2 by A3, A8, A56, GOBOARD5:1;
then A60: p `2 = (((GoB f) * (1,(width (GoB f)))) `2) + 1 by EUCLID:52;
then A61: ((GoB f) * (1,(width (GoB f)))) `2 < p `2 by XREAL_1:29;
p in { |[r,s]| where r, s is Real : ((GoB f) * (1,(width (GoB f)))) `2 <= s }

proof

p = |[(p `1),(p `2)]| by EUCLID:53;
hence p in { |[r,s]| where r, s is Real : ((GoB f) * (1,(width (GoB f)))) `2 <= s } by A61; :: thesis:

end;

then A62: p in h_strip ((GoB f),j2) by A55, A58, GOBOARD5:6;
((GoB f) * (1,(width (GoB f)))) `2 < (((GoB f) * (1,(width (GoB f)))) `2) + 1 by XREAL_1:29;
then A63: ( p in {p} & {p} c= (L~ f) ` ) by A60, A57, SUBSET_1:23, TARSKI:def 1;
then reconsider p1 = p as Point of ((TOP-REAL 2) | ((L~ f) `)) by PRE_TOPC:8;
A64: ( i1 = 0 or i1 >= 0 + 1 ) by NAT_1:13;

A65: now :: thesis:

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

case A66: ( i1 >= 1 & i1 + 1 < len (GoB f) ) ; :: thesis:

then A67: (i1 + 1) + 1 <= len (GoB f) by NAT_1:13;
A68: p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i1 + 1),(width (GoB f)))) `1 <= r & r <= ((GoB f) * (((i1 + 1) + 1),(width (GoB f)))) `1 ) }

proof

i1 + 1 < (i1 + 1) + 1 by NAT_1:13;
then ((GoB f) * ((i1 + 1),(width (GoB f)))) `1 <= ((GoB f) * (((i1 + 1) + 1),(width (GoB f)))) `1 by A56, A59, A67, GOBOARD5:3;
hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i1 + 1),(width (GoB f)))) `1 <= r & r <= ((GoB f) * (((i1 + 1) + 1),(width (GoB f)))) `1 ) } ; :: thesis:

end;

1 <= i1 + 1 by NAT_1:11;
then p in v_strip ((GoB f),(i1 + 1)) by A56, A66, A68, GOBOARD5:8;
then p in (v_strip ((GoB f),(i1 + 1))) /\ (h_strip ((GoB f),j2)) by A62, XBOOLE_0:def 4;
then A69: p in cell ((GoB f),(i1 + 1),j2) by GOBOARD5:def 3;
A70: p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i1,(width (GoB f)))) `1 <= r & r <= ((GoB f) * ((i1 + 1),(width (GoB f)))) `1 ) }

proof

i1 < i1 + 1 by NAT_1:13;
then ((GoB f) * (i1,(width (GoB f)))) `1 < ((GoB f) * ((i1 + 1),(width (GoB f)))) `1 by A56, A66, GOBOARD5:3;
hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i1,(width (GoB f)))) `1 <= r & r <= ((GoB f) * ((i1 + 1),(width (GoB f)))) `1 ) } ; :: thesis:

end;

i1 < len (GoB f) by A66, NAT_1:13;
then p in v_strip ((GoB f),i1) by A56, A66, A70, GOBOARD5:8;
then p in (v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j2)) by A62, XBOOLE_0:def 4;
then p in cell ((GoB f),i1,j2) by GOBOARD5:def 3;
hence ( p in (cell ((GoB f),(i1 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i1,j2)) /\ ((L~ f) `) ) by A63, A69, XBOOLE_0:def 4; :: thesis:

end;

case A71: ( i1 >= 1 & i1 + 1 = len (GoB f) ) ; :: thesis:

A72: i1 < i1 + 1 by NAT_1:13;
A73: p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i1,(width (GoB f)))) `1 <= r & r <= ((GoB f) * ((i1 + 1),(width (GoB f)))) `1 ) }

proof

((GoB f) * (i1,(width (GoB f)))) `1 < ((GoB f) * ((i1 + 1),(width (GoB f)))) `1 by A56, A71, A72, GOBOARD5:3;
hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i1,(width (GoB f)))) `1 <= r & r <= ((GoB f) * ((i1 + 1),(width (GoB f)))) `1 ) } ; :: thesis:

end;

p in { |[r,s]| where r, s is Real : ((GoB f) * ((i1 + 1),(width (GoB f)))) `1 <= r } ;
then p in v_strip ((GoB f),(i1 + 1)) by A56, A71, GOBOARD5:9;
then p in (v_strip ((GoB f),(i1 + 1))) /\ (h_strip ((GoB f),j2)) by A62, XBOOLE_0:def 4;
then A74: p in cell ((GoB f),(i1 + 1),j2) by GOBOARD5:def 3;
i1 < len (GoB f) by A71, NAT_1:13;
then p in v_strip ((GoB f),i1) by A56, A71, A73, GOBOARD5:8;
then p in (v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j2)) by A62, XBOOLE_0:def 4;
then p in cell ((GoB f),i1,j2) by GOBOARD5:def 3;
hence ( p in (cell ((GoB f),(i1 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i1,j2)) /\ ((L~ f) `) ) by A63, A74, XBOOLE_0:def 4; :: thesis:

end;

case A75: ( i1 = 0 & i1 + 1 < len (GoB f) ) ; :: thesis:

then A76: (i1 + 1) + 1 <= len (GoB f) by NAT_1:13;
p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i1 + 1),(width (GoB f)))) `1 <= r & r <= ((GoB f) * (((i1 + 1) + 1),(width (GoB f)))) `1 ) }

proof

i1 + 1 < (i1 + 1) + 1 by NAT_1:13;
then ((GoB f) * ((i1 + 1),(width (GoB f)))) `1 <= ((GoB f) * (((i1 + 1) + 1),(width (GoB f)))) `1 by A56, A59, A76, GOBOARD5:3;
hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i1 + 1),(width (GoB f)))) `1 <= r & r <= ((GoB f) * (((i1 + 1) + 1),(width (GoB f)))) `1 ) } ; :: thesis:

end;

then p in v_strip ((GoB f),(i1 + 1)) by A56, A75, GOBOARD5:8;
then p in (v_strip ((GoB f),(i1 + 1))) /\ (h_strip ((GoB f),j2)) by A62, XBOOLE_0:def 4;
then A77: p in cell ((GoB f),(i1 + 1),j2) by GOBOARD5:def 3;
p in { |[r,s]| where r, s is Real : r <= ((GoB f) * (1,(width (GoB f)))) `1 } by A75;
then p in v_strip ((GoB f),i1) by A56, A75, GOBOARD5:10;
then p in (v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j2)) by A62, XBOOLE_0:def 4;
then p in cell ((GoB f),i1,j2) by GOBOARD5:def 3;
hence ( p in (cell ((GoB f),(i1 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i1,j2)) /\ ((L~ f) `) ) by A63, A77, XBOOLE_0:def 4; :: thesis:

end;

case ( i1 = 0 & i1 + 1 = len (GoB f) ) ; :: thesis:

hence contradiction by GOBOARD7:32; :: thesis:

end;

end;

case A85: ( j2 <> 0 & j2 <> width (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) * ((i1 + 1),j2)),((GoB f) * ((i1 + 1),(j2 + 1)))) ) ) ) ; :: thesis:

then A86: j2 < width (GoB f) by A4, XXREAL_0:1;
then A87: j2 + 1 <= width (GoB f) by NAT_1:13;
for k being Nat st 1 <= k & k + 1 <= len f holds
LSeg (((GoB f) * ((i1 + 1),j2)),((GoB f) * ((i1 + 1),(j2 + 1)))) <> LSeg (f,k)

proof

let k be 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) * ((i1 + 1),j2)),((GoB f) * ((i1 + 1),(j2 + 1)))) <> LSeg (f,k) by A85, A88; :: thesis:

end;

then A89: ( 1 <= i1 + 1 & i1 + 1 <= len (GoB f) & 1 <= j2 & j2 + 1 <= width (GoB f) implies not (1 / 2) * (((GoB f) * ((i1 + 1),j2)) + ((GoB f) * ((i1 + 1),(j2 + 1)))) in L~ f ) by GOBOARD7:39;
reconsider p = (1 / 2) * (((GoB f) * ((i1 + 1),j2)) + ((GoB f) * ((i1 + 1),(j2 + 1)))) as Point of (TOP-REAL 2) ;
A90: p `2 = (1 / 2) * ((((GoB f) * ((i1 + 1),j2)) + ((GoB f) * ((i1 + 1),(j2 + 1)))) `2) by TOPREAL3:4
.= (1 / 2) * ((((GoB f) * ((i1 + 1),j2)) `2) + (((GoB f) * ((i1 + 1),(j2 + 1))) `2)) by TOPREAL3:2 ;
reconsider P = {p} as Subset of (TOP-REAL 2) ;
A91: 1 < width (GoB f) by GOBOARD7:33;
Down ((RightComp f),((L~ f) `)) is closed by Lm4, CONNSP_1:33;
then A92: Cl (Down ((RightComp f),((L~ f) `))) = Down ((RightComp f),((L~ f) `)) by PRE_TOPC:22;
Down ((LeftComp f),((L~ f) `)) is closed by Lm3, CONNSP_1:33;
then A93: Cl (Down ((LeftComp f),((L~ f) `))) = Down ((LeftComp f),((L~ f) `)) by PRE_TOPC:22;
(Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) = Down (((LeftComp f) \/ (RightComp f)),((L~ f) `)) by GOBRD11:4;
then A94: Cl (Down (((LeftComp f) \/ (RightComp f)),((L~ f) `))) = (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A93, A92, PRE_TOPC:20;
A95: ( Down ((LeftComp f),((L~ f) `)) = LeftComp f & Down ((RightComp f),((L~ f) `)) = RightComp f ) by Th5;
Down ((Int (cell ((GoB f),i1,j2))),((L~ f) `)) c= (LeftComp f) \/ (RightComp f) by A1, A2, A6, A7, Th3;
then Down ((Int (cell ((GoB f),i1,j2))),((L~ f) `)) c= Down (((LeftComp f) \/ (RightComp f)),((L~ f) `)) by A95, GOBRD11:4;
then A96: Cl (Down ((Int (cell ((GoB f),i1,j2))),((L~ f) `))) c= Cl (Down (((LeftComp f) \/ (RightComp f)),((L~ f) `))) by PRE_TOPC:19;
A97: ( Down ((Int (cell ((GoB f),(i1 + 1),j2))),((L~ f) `)) c= Cl (Down ((Int (cell ((GoB f),(i1 + 1),j2))),((L~ f) `))) & Down ((Int (cell ((GoB f),(i1 + 1),j2))),((L~ f) `)) = Int (cell ((GoB f),(i1 + 1),j2)) ) by A3, A4, A8, Th3, PRE_TOPC:18;
A98: 1 <= i1 + 1 by NAT_1:11;
A99: 0 + 1 <= j2 by A85, NAT_1:13;
then A100: 1 < j2 + 1 by NAT_1:13;
( ( for x being 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 A3, A8, A99, A86, A89, NAT_1:13, SUBSET_1:23, TARSKI:def 1;
then reconsider p1 = p as Point of ((TOP-REAL 2) | ((L~ f) `)) by PRE_TOPC:8;
A102: 1 <= 1 + i1 by NAT_1:11;
p `1 = (1 / 2) * ((((GoB f) * ((i1 + 1),j2)) + ((GoB f) * ((i1 + 1),(j2 + 1)))) `1) by TOPREAL3:4
.= (1 / 2) * ((((GoB f) * ((i1 + 1),j2)) `1) + (((GoB f) * ((i1 + 1),(j2 + 1))) `1)) by TOPREAL3:2 ;
then A103: p = |[((1 / 2) * ((((GoB f) * ((i1 + 1),j2)) `1) + (((GoB f) * ((i1 + 1),(j2 + 1))) `1))),((1 / 2) * ((((GoB f) * ((i1 + 1),j2)) `2) + (((GoB f) * ((i1 + 1),(j2 + 1))) `2)))]| by A90, EUCLID:53;
j2 < j2 + 1 by NAT_1:13;
then A104: ((GoB f) * ((i1 + 1),j2)) `2 < ((GoB f) * ((i1 + 1),(j2 + 1))) `2 by A3, A8, A99, A87, A102, GOBOARD5:4;
then (((GoB f) * ((i1 + 1),j2)) `2) + (((GoB f) * ((i1 + 1),(j2 + 1))) `2) < (((GoB f) * ((i1 + 1),(j2 + 1))) `2) + (((GoB f) * ((i1 + 1),(j2 + 1))) `2) by XREAL_1:8;
then A105: ((((GoB f) * ((i1 + 1),j2)) `2) + (((GoB f) * ((i1 + 1),(j2 + 1))) `2)) / 2 < ((((GoB f) * ((i1 + 1),(j2 + 1))) `2) + (((GoB f) * ((i1 + 1),(j2 + 1))) `2)) / 2 by XREAL_1:74;
(((GoB f) * ((i1 + 1),j2)) `2) + (((GoB f) * ((i1 + 1),j2)) `2) < (((GoB f) * ((i1 + 1),j2)) `2) + (((GoB f) * ((i1 + 1),(j2 + 1))) `2) by A104, XREAL_1:8;
then A106: ((((GoB f) * ((i1 + 1),j2)) `2) + (((GoB f) * ((i1 + 1),j2)) `2)) / 2 < ((((GoB f) * ((i1 + 1),j2)) `2) + (((GoB f) * ((i1 + 1),(j2 + 1))) `2)) / 2 by XREAL_1:74;
p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i1 + 1),j2)) `2 <= s & s <= ((GoB f) * ((i1 + 1),(j2 + 1))) `2 ) }

proof

p = |[(p `1),(p `2)]| by EUCLID:53;
hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i1 + 1),j2)) `2 <= s & s <= ((GoB f) * ((i1 + 1),(j2 + 1))) `2 ) } by A90, A106, A105; :: thesis:

end;

then A107: p in h_strip ((GoB f),j2) by A3, A8, A99, A86, A98, GOBOARD5:5;
A108: ( i1 = 0 or i1 >= 0 + 1 ) by NAT_1:13;

A109: now :: thesis:

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

case A110: ( i1 >= 1 & i1 + 1 < len (GoB f) ) ; :: thesis:

then A111: (i1 + 1) + 1 <= len (GoB f) by NAT_1:13;
A112: p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i1 + 1),1)) `1 <= r & r <= ((GoB f) * (((i1 + 1) + 1),1)) `1 ) }

proof

i1 + 1 < (i1 + 1) + 1 by NAT_1:13;
then A113: ((GoB f) * ((i1 + 1),1)) `1 < ((GoB f) * (((i1 + 1) + 1),1)) `1 by A91, A102, A111, GOBOARD5:3;
( ((GoB f) * ((i1 + 1),j2)) `1 = ((GoB f) * ((i1 + 1),1)) `1 & ((GoB f) * ((i1 + 1),(j2 + 1))) `1 = ((GoB f) * ((i1 + 1),1)) `1 ) by A3, A4, A8, A99, A87, A102, A100, GOBOARD5:2;
hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i1 + 1),1)) `1 <= r & r <= ((GoB f) * (((i1 + 1) + 1),1)) `1 ) } by A103, A113; :: thesis:

end;

1 <= i1 + 1 by NAT_1:11;
then p in v_strip ((GoB f),(i1 + 1)) by A91, A110, A112, GOBOARD5:8;
then p in (v_strip ((GoB f),(i1 + 1))) /\ (h_strip ((GoB f),j2)) by A107, XBOOLE_0:def 4;
then A114: p in cell ((GoB f),(i1 + 1),j2) by GOBOARD5:def 3;
A115: p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i1,1)) `1 <= r & r <= ((GoB f) * ((i1 + 1),1)) `1 ) }

proof

i1 < i1 + 1 by NAT_1:13;
then A116: ((GoB f) * (i1,1)) `1 < ((GoB f) * ((i1 + 1),1)) `1 by A91, A110, GOBOARD5:3;
( ((GoB f) * ((i1 + 1),j2)) `1 = ((GoB f) * ((i1 + 1),1)) `1 & ((GoB f) * ((i1 + 1),(j2 + 1))) `1 = ((GoB f) * ((i1 + 1),1)) `1 ) by A3, A4, A8, A99, A87, A102, A100, GOBOARD5:2;
hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i1,1)) `1 <= r & r <= ((GoB f) * ((i1 + 1),1)) `1 ) } by A103, A116; :: thesis:

end;

i1 < len (GoB f) by A110, NAT_1:13;
then p in v_strip ((GoB f),i1) by A91, A110, A115, GOBOARD5:8;
then p in (v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j2)) by A107, XBOOLE_0:def 4;
then p in cell ((GoB f),i1,j2) by GOBOARD5:def 3;
hence ( p in (cell ((GoB f),(i1 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i1,j2)) /\ ((L~ f) `) ) by A101, A114, XBOOLE_0:def 4; :: thesis:

end;

case A117: ( i1 >= 1 & i1 + 1 = len (GoB f) ) ; :: thesis:

A118: i1 < i1 + 1 by NAT_1:13;
p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i1,1)) `1 <= r & r <= ((GoB f) * ((i1 + 1),1)) `1 ) }

proof

A119: ((GoB f) * (i1,1)) `1 < ((GoB f) * ((i1 + 1),1)) `1 by A91, A117, A118, GOBOARD5:3;
( ((GoB f) * ((i1 + 1),j2)) `1 = ((GoB f) * ((i1 + 1),1)) `1 & ((GoB f) * ((i1 + 1),(j2 + 1))) `1 = ((GoB f) * ((i1 + 1),1)) `1 ) by A3, A4, A8, A99, A87, A102, A100, GOBOARD5:2;
hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i1,1)) `1 <= r & r <= ((GoB f) * ((i1 + 1),1)) `1 ) } by A103, A119; :: thesis:

end;

then p in v_strip ((GoB f),i1) by A91, A117, A118, GOBOARD5:8;
then p in (v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j2)) by A107, XBOOLE_0:def 4;
then A120: p in cell ((GoB f),i1,j2) by GOBOARD5:def 3;
p in { |[r,s]| where r, s is Real : ((GoB f) * ((i1 + 1),1)) `1 <= r }

proof

( ((GoB f) * ((i1 + 1),j2)) `1 = ((GoB f) * ((i1 + 1),1)) `1 & ((GoB f) * ((i1 + 1),(j2 + 1))) `1 = ((GoB f) * ((i1 + 1),1)) `1 ) by A3, A4, A8, A99, A87, A102, A100, GOBOARD5:2;
hence p in { |[r,s]| where r, s is Real : ((GoB f) * ((i1 + 1),1)) `1 <= r } by A103; :: thesis:

end;

then p in v_strip ((GoB f),(i1 + 1)) by A91, A117, GOBOARD5:9;
then p in (v_strip ((GoB f),(i1 + 1))) /\ (h_strip ((GoB f),j2)) by A107, XBOOLE_0:def 4;
then p in cell ((GoB f),(i1 + 1),j2) by GOBOARD5:def 3;
hence ( p in (cell ((GoB f),(i1 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i1,j2)) /\ ((L~ f) `) ) by A101, A120, XBOOLE_0:def 4; :: thesis:

end;

case A121: ( i1 = 0 & i1 + 1 < len (GoB f) ) ; :: thesis:

then A122: (i1 + 1) + 1 <= len (GoB f) by NAT_1:13;
p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i1 + 1),1)) `1 <= r & r <= ((GoB f) * (((i1 + 1) + 1),1)) `1 ) }

proof

i1 + 1 < (i1 + 1) + 1 by NAT_1:13;
then A123: ((GoB f) * ((i1 + 1),1)) `1 < ((GoB f) * (((i1 + 1) + 1),1)) `1 by A91, A102, A122, GOBOARD5:3;
( ((GoB f) * ((i1 + 1),j2)) `1 = ((GoB f) * ((i1 + 1),1)) `1 & ((GoB f) * ((i1 + 1),(j2 + 1))) `1 = ((GoB f) * ((i1 + 1),1)) `1 ) by A3, A4, A8, A99, A87, A102, A100, GOBOARD5:2;
hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i1 + 1),1)) `1 <= r & r <= ((GoB f) * (((i1 + 1) + 1),1)) `1 ) } by A103, A123; :: thesis:

end;

then p in v_strip ((GoB f),(i1 + 1)) by A91, A121, GOBOARD5:8;
then p in (v_strip ((GoB f),(i1 + 1))) /\ (h_strip ((GoB f),j2)) by A107, XBOOLE_0:def 4;
then A124: p in cell ((GoB f),(i1 + 1),j2) by GOBOARD5:def 3;
p in { |[r,s]| where r, s is Real : r <= ((GoB f) * (1,1)) `1 }

proof

( ((GoB f) * ((i1 + 1),j2)) `1 = ((GoB f) * ((i1 + 1),1)) `1 & ((GoB f) * ((i1 + 1),(j2 + 1))) `1 = ((GoB f) * ((i1 + 1),1)) `1 ) by A3, A4, A8, A99, A87, A102, A100, GOBOARD5:2;
hence p in { |[r,s]| where r, s is Real : r <= ((GoB f) * (1,1)) `1 } by A103, A121; :: thesis:

end;

then p in v_strip ((GoB f),i1) by A91, A121, GOBOARD5:10;
then p in (v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j2)) by A107, XBOOLE_0:def 4;
then p in cell ((GoB f),i1,j2) by GOBOARD5:def 3;
hence ( p in (cell ((GoB f),(i1 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i1,j2)) /\ ((L~ f) `) ) by A101, A124, XBOOLE_0:def 4; :: thesis:

end;

case ( i1 = 0 & i1 + 1 = len (GoB f) ) ; :: thesis:

hence contradiction by GOBOARD7:32; :: thesis:

end;

then p in Cl (Down ((Int (cell ((GoB f),(i1 + 1),j2))),((L~ f) `))) by A4, Th2;
then A125: Cl (Down ((Int (cell ((GoB f),(i1 + 1),j2))),((L~ f) `))) c= Component_of p1 by A3, A4, A8, Th3, GOBRD11:1;
p in Cl (Down ((Int (cell ((GoB f),i1,j2))),((L~ f) `))) by A1, A4, A109, Th2;
then Component_of p1 c= (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A96, A94, Th5, CONNSP_3:21;
then Cl (Down ((Int (cell ((GoB f),(i1 + 1),j2))),((L~ f) `))) c= (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A125;
hence Int (cell ((GoB f),(i1 + 1),j2)) c= (LeftComp f) \/ (RightComp f) by A95, A97; :: thesis:

end;

hence Int (cell ((GoB f),(i1 + 1),j2)) 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: i1 = i2 + 1 ; :: thesis:

then i2 < i1 by NAT_1:13;
then A127: i1 -' 1 < i1 by A126, NAT_D:34;
A128: i2 < i2 + 1 by NAT_1:13;
A129: 1 <= (i1 -' 1) + 1 by NAT_1:11;
A130: i2 + 1 < (i2 + 1) + 1 by NAT_1:13;
A131: ( 1 <= i1 & i1 -' 1 = i1 - 1 ) by A126, NAT_1:11, XREAL_0:def 2;
A132: 1 <= i2 + 1 by NAT_1:11;
A133: i1 -' 1 = i2 by A126, NAT_D:34;

now :: thesis:

per cases ;

case ex k being Nat st
( 1 <= k & k + 1 <= len f & j2 <> 0 & j2 <> width (GoB f) & LSeg ((f /. k),(f /. (k + 1))) = LSeg (((GoB f) * ((i2 + 1),j2)),((GoB f) * ((i2 + 1),(j2 + 1)))) ) ; :: thesis:

then consider k being Nat such that
A134: ( 1 <= k & k + 1 <= len f ) and
A135: j2 <> 0 and
A136: j2 <> width (GoB f) and
A137: LSeg ((f /. k),(f /. (k + 1))) = LSeg (((GoB f) * (((i1 -' 1) + 1),j2)),((GoB f) * (((i1 -' 1) + 1),(j2 + 1)))) by A133;

now :: thesis:

per cases by A137, SPPOL_1:8;

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

A139: ( Int (left_cell (f,k)) c= LeftComp f & LeftComp f c= (LeftComp f) \/ (RightComp f) ) by A134, GOBOARD9:21, XBOOLE_1:7;
j2 < width (GoB f) by A4, A136, XXREAL_0:1;
then A140: j2 + 1 <= width (GoB f) by NAT_1:13;
i1 -' 1 < len (GoB f) by A1, A127, XXREAL_0:2;
then (i1 -' 1) + 1 <= len (GoB f) by NAT_1:13;
then A141: ( Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] & (i1 -' 1) + 1 in dom (GoB f) ) by A129, FINSEQ_3:25, MATRIX_0:def 4;
1 <= j2 + 1 by NAT_1:11;
then j2 + 1 in Seg (width (GoB f)) by A140, FINSEQ_1:1;
then A142: [((i1 -' 1) + 1),(j2 + 1)] in Indices (GoB f) by A141, ZFMISC_1:87;
j2 >= 0 + 1 by A135, NAT_1:13;
then j2 in Seg (width (GoB f)) by A4, FINSEQ_1:1;
then [((i1 -' 1) + 1),j2] in Indices (GoB f) by A141, ZFMISC_1:87;
then left_cell (f,k) = cell ((GoB f),(i1 -' 1),j2) by A134, A138, A142, GOBOARD5:27;
hence Int (cell ((GoB f),(i1 -' 1),j2)) c= (LeftComp f) \/ (RightComp f) by A139; :: thesis:

end;

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

A144: ( Int (right_cell (f,k)) c= RightComp f & RightComp f c= (LeftComp f) \/ (RightComp f) ) by A134, GOBOARD9:25, XBOOLE_1:7;
j2 < width (GoB f) by A4, A136, XXREAL_0:1;
then A145: j2 + 1 <= width (GoB f) by NAT_1:13;
A146: ( Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] & (i1 -' 1) + 1 in dom (GoB f) ) by A1, A131, FINSEQ_3:25, MATRIX_0:def 4;
1 <= j2 + 1 by NAT_1:11;
then j2 + 1 in Seg (width (GoB f)) by A145, FINSEQ_1:1;
then A147: [((i1 -' 1) + 1),(j2 + 1)] in Indices (GoB f) by A146, ZFMISC_1:87;
j2 >= 0 + 1 by A135, NAT_1:13;
then j2 in Seg (width (GoB f)) by A4, FINSEQ_1:1;
then [((i1 -' 1) + 1),j2] in Indices (GoB f) by A146, ZFMISC_1:87;
then right_cell (f,k) = cell ((GoB f),(i1 -' 1),j2) by A134, A143, A147, GOBOARD5:30;
hence Int (cell ((GoB f),(i1 -' 1),j2)) c= (LeftComp f) \/ (RightComp f) by A144; :: 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 j2 <> 0 or not j2 <> width (GoB f) or not LSeg ((f /. k),(f /. (k + 1))) = LSeg (((GoB f) * ((i2 + 1),j2)),((GoB f) * ((i2 + 1),(j2 + 1)))) ) ; :: thesis:

now :: thesis:

per cases by A148;

case A149: j2 = 0 ; :: thesis:

reconsider p = |[(((GoB f) * ((i2 + 1),1)) `1),((((GoB f) * ((i2 + 1),1)) `2) - 1)]| as Point of (TOP-REAL 2) ;
A150: 1 < width (GoB f) by GOBOARD7:33;
A151: 1 < len (GoB f) by GOBOARD7:32;
reconsider P = {p} as Subset of (TOP-REAL 2) ;
A152: p `2 < (p `2) + 1 by XREAL_1:29;
A153: 1 <= i2 + 1 by NAT_1:11;
then ((GoB f) * ((i2 + 1),1)) `2 = ((GoB f) * (1,1)) `2 by A1, A126, A150, GOBOARD5:1;
then A154: p `2 = (((GoB f) * (1,1)) `2) - 1 by EUCLID:52;
p in { |[r,s]| where r, s is Real : s <= ((GoB f) * (1,1)) `2 }

proof

p = |[(p `1),(p `2)]| by EUCLID:53;
hence p in { |[r,s]| where r, s is Real : s <= ((GoB f) * (1,1)) `2 } by A154, A152; :: thesis:

end;

then A155: p in h_strip ((GoB f),j2) by A149, A151, GOBOARD5:7;
( ( for q being Point of (TOP-REAL 2) st q in P holds
q `2 < ((GoB f) * (1,1)) `2 ) implies P misses L~ f ) by GOBOARD8:23;
then A156: ( p in {p} & {p} c= (L~ f) ` ) by A154, A152, SUBSET_1:23, TARSKI:def 1;
then reconsider p1 = p as Point of ((TOP-REAL 2) | ((L~ f) `)) by PRE_TOPC:8;

A157: now :: thesis:

per cases by A1, A126, XXREAL_0:1;

case A158: ( i2 + 1 < len (GoB f) & i2 > 0 ) ; :: thesis:

then A159: (i2 + 1) + 1 <= len (GoB f) by NAT_1:13;
A160: p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i2 + 1),1)) `1 <= r & r <= ((GoB f) * (((i2 + 1) + 1),1)) `1 ) }

proof

i2 + 1 < (i2 + 1) + 1 by NAT_1:13;
then ((GoB f) * ((i2 + 1),1)) `1 <= ((GoB f) * (((i2 + 1) + 1),1)) `1 by A150, A153, A159, GOBOARD5:3;
hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i2 + 1),1)) `1 <= r & r <= ((GoB f) * (((i2 + 1) + 1),1)) `1 ) } ; :: thesis:

end;

A161: 0 + 1 <= i2 by A158, NAT_1:13;
A162: p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i2,1)) `1 <= r & r <= ((GoB f) * ((i2 + 1),1)) `1 ) }

proof

i2 < i2 + 1 by NAT_1:13;
then ((GoB f) * (i2,1)) `1 < ((GoB f) * ((i2 + 1),1)) `1 by A1, A126, A150, A161, GOBOARD5:3;
hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i2,1)) `1 <= r & r <= ((GoB f) * ((i2 + 1),1)) `1 ) } ; :: thesis:

end;

i2 < len (GoB f) by A158, NAT_1:13;
then p in v_strip ((GoB f),i2) by A150, A161, A162, GOBOARD5:8;
then p in (v_strip ((GoB f),i2)) /\ (h_strip ((GoB f),j2)) by A155, XBOOLE_0:def 4;
then A163: p in cell ((GoB f),i2,j2) by GOBOARD5:def 3;
1 <= i2 + 1 by A161, NAT_1:13;
then p in v_strip ((GoB f),(i2 + 1)) by A150, A158, A160, GOBOARD5:8;
then p in (v_strip ((GoB f),(i2 + 1))) /\ (h_strip ((GoB f),j2)) by A155, XBOOLE_0:def 4;
then p in cell ((GoB f),(i2 + 1),j2) by GOBOARD5:def 3;
hence ( p in (cell ((GoB f),(i2 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) by A156, A163, XBOOLE_0:def 4; :: thesis:

end;

case A164: ( i2 + 1 < len (GoB f) & i2 = 0 ) ; :: thesis:

A165: i2 + 1 < (i2 + 1) + 1 by NAT_1:13;
A166: (i2 + 1) + 1 <= len (GoB f) by A164, NAT_1:13;
p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i2 + 1),1)) `1 <= r & r <= ((GoB f) * (((i2 + 1) + 1),1)) `1 ) }

proof

((GoB f) * ((i2 + 1),1)) `1 < ((GoB f) * (((i2 + 1) + 1),1)) `1 by A132, A150, A166, A165, GOBOARD5:3;
hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i2 + 1),1)) `1 <= r & r <= ((GoB f) * (((i2 + 1) + 1),1)) `1 ) } ; :: thesis:

end;

then p in v_strip ((GoB f),(i2 + 1)) by A150, A164, GOBOARD5:8;
then p in (v_strip ((GoB f),(i2 + 1))) /\ (h_strip ((GoB f),j2)) by A155, XBOOLE_0:def 4;
then A167: p in cell ((GoB f),(i2 + 1),j2) by GOBOARD5:def 3;
p in { |[r,s]| where r, s is Real : r <= ((GoB f) * ((i2 + 1),1)) `1 } ;
then p in v_strip ((GoB f),i2) by A150, A164, GOBOARD5:10;
then p in (v_strip ((GoB f),i2)) /\ (h_strip ((GoB f),j2)) by A155, XBOOLE_0:def 4;
then p in cell ((GoB f),i2,j2) by GOBOARD5:def 3;
hence ( p in (cell ((GoB f),(i2 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) by A156, A167, XBOOLE_0:def 4; :: thesis:

end;

case A168: ( i2 + 1 = len (GoB f) & i2 > 0 ) ; :: thesis:

then A169: 0 + 1 <= i2 by NAT_1:13;
A170: p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i2,1)) `1 <= r & r <= ((GoB f) * ((i2 + 1),1)) `1 ) }

proof

((GoB f) * (i2,1)) `1 < ((GoB f) * ((i2 + 1),1)) `1 by A128, A150, A168, A169, GOBOARD5:3;
hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i2,1)) `1 <= r & r <= ((GoB f) * ((i2 + 1),1)) `1 ) } ; :: thesis:

end;

p in { |[r,s]| where r, s is Real : ((GoB f) * ((i2 + 1),1)) `1 <= r } ;
then p in v_strip ((GoB f),(i2 + 1)) by A150, A168, GOBOARD5:9;
then p in (v_strip ((GoB f),(i2 + 1))) /\ (h_strip ((GoB f),j2)) by A155, XBOOLE_0:def 4;
then A171: p in cell ((GoB f),(i2 + 1),j2) by GOBOARD5:def 3;
i2 < len (GoB f) by A168, NAT_1:13;
then p in v_strip ((GoB f),i2) by A150, A169, A170, GOBOARD5:8;
then p in (v_strip ((GoB f),i2)) /\ (h_strip ((GoB f),j2)) by A155, XBOOLE_0:def 4;
then p in cell ((GoB f),i2,j2) by GOBOARD5:def 3;
hence ( p in (cell ((GoB f),(i2 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) by A156, A171, XBOOLE_0:def 4; :: thesis:

end;

case A172: ( i2 + 1 = len (GoB f) & i2 = 0 ) ; :: thesis:

p in { |[r,s]| where r, s is Real : ((GoB f) * ((i2 + 1),1)) `1 <= r } ;
then p in v_strip ((GoB f),(i2 + 1)) by A150, A172, GOBOARD5:9;
then p in (v_strip ((GoB f),(i2 + 1))) /\ (h_strip ((GoB f),j2)) by A155, XBOOLE_0:def 4;
then A173: p in cell ((GoB f),(i2 + 1),j2) by GOBOARD5:def 3;
p in { |[r,s]| where r, s is Real : r <= ((GoB f) * (1,1)) `1 } by A172;
then p in v_strip ((GoB f),i2) by A150, A172, GOBOARD5:10;
then p in (v_strip ((GoB f),i2)) /\ (h_strip ((GoB f),j2)) by A155, XBOOLE_0:def 4;
then p in cell ((GoB f),i2,j2) by GOBOARD5:def 3;
hence ( p in (cell ((GoB f),(i2 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) by A156, A173, XBOOLE_0:def 4; :: thesis:

end;

end;

case A181: j2 = width (GoB f) ; :: thesis:

reconsider p = |[(((GoB f) * ((i2 + 1),(width (GoB f)))) `1),((((GoB f) * ((i2 + 1),(width (GoB f)))) `2) + 1)]| as Point of (TOP-REAL 2) ;
A182: 1 < width (GoB f) by GOBOARD7:33;
reconsider P = {p} as Subset of (TOP-REAL 2) ;
A183: ( ( for q being Point of (TOP-REAL 2) st q in P holds
((GoB f) * (1,(width (GoB f)))) `2 < q `2 ) implies P misses L~ f ) by GOBOARD8:24;
A184: 1 < len (GoB f) by GOBOARD7:32;
A185: 1 <= i2 + 1 by NAT_1:11;
then ((GoB f) * ((i2 + 1),(width (GoB f)))) `2 = ((GoB f) * (1,(width (GoB f)))) `2 by A1, A126, A182, GOBOARD5:1;
then A186: p `2 = (((GoB f) * (1,(width (GoB f)))) `2) + 1 by EUCLID:52;
p in { |[r,s]| where r, s is Real : ((GoB f) * (1,(width (GoB f)))) `2 <= s }

proof

( p = |[(p `1),(p `2)]| & ((GoB f) * (1,(width (GoB f)))) `2 <= p `2 ) by A186, EUCLID:53, XREAL_1:29;
hence p in { |[r,s]| where r, s is Real : ((GoB f) * (1,(width (GoB f)))) `2 <= s } ; :: thesis:

end;

then A187: p in h_strip ((GoB f),j2) by A181, A184, GOBOARD5:6;
((GoB f) * (1,(width (GoB f)))) `2 < (((GoB f) * (1,(width (GoB f)))) `2) + 1 by XREAL_1:29;
then A188: ( p in {p} & {p} c= (L~ f) ` ) by A186, A183, SUBSET_1:23, TARSKI:def 1;
then reconsider p1 = p as Point of ((TOP-REAL 2) | ((L~ f) `)) by PRE_TOPC:8;

A189: now :: thesis:

per cases by A1, A126, XXREAL_0:1;

case A190: ( i2 + 1 < len (GoB f) & i2 > 0 ) ; :: thesis:

then A191: (i2 + 1) + 1 <= len (GoB f) by NAT_1:13;
A192: p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i2 + 1),(width (GoB f)))) `1 <= r & r <= ((GoB f) * (((i2 + 1) + 1),(width (GoB f)))) `1 ) }

proof

i2 + 1 < (i2 + 1) + 1 by NAT_1:13;
then ((GoB f) * ((i2 + 1),(width (GoB f)))) `1 <= ((GoB f) * (((i2 + 1) + 1),(width (GoB f)))) `1 by A182, A185, A191, GOBOARD5:3;
hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i2 + 1),(width (GoB f)))) `1 <= r & r <= ((GoB f) * (((i2 + 1) + 1),(width (GoB f)))) `1 ) } ; :: thesis:

end;

1 <= i2 + 1 by NAT_1:11;
then p in v_strip ((GoB f),(i2 + 1)) by A182, A190, A192, GOBOARD5:8;
then p in (v_strip ((GoB f),(i2 + 1))) /\ (h_strip ((GoB f),j2)) by A187, XBOOLE_0:def 4;
then A193: p in cell ((GoB f),(i2 + 1),j2) by GOBOARD5:def 3;
A194: 0 + 1 <= i2 by A190, NAT_1:13;
A195: i2 < i2 + 1 by NAT_1:13;
A196: p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i2,(width (GoB f)))) `1 <= r & r <= ((GoB f) * ((i2 + 1),(width (GoB f)))) `1 ) }

proof

((GoB f) * (i2,(width (GoB f)))) `1 < ((GoB f) * ((i2 + 1),(width (GoB f)))) `1 by A1, A126, A182, A194, A195, GOBOARD5:3;
hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i2,(width (GoB f)))) `1 <= r & r <= ((GoB f) * ((i2 + 1),(width (GoB f)))) `1 ) } ; :: thesis:

end;

i2 < len (GoB f) by A190, NAT_1:13;
then p in v_strip ((GoB f),i2) by A182, A194, A196, GOBOARD5:8;
then p in (v_strip ((GoB f),i2)) /\ (h_strip ((GoB f),j2)) by A187, XBOOLE_0:def 4;
then p in cell ((GoB f),i2,j2) by GOBOARD5:def 3;
hence ( p in (cell ((GoB f),(i2 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) by A188, A193, XBOOLE_0:def 4; :: thesis:

end;

case A197: ( i2 + 1 < len (GoB f) & i2 = 0 ) ; :: thesis:

then A198: (i2 + 1) + 1 <= len (GoB f) by NAT_1:13;
p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i2 + 1),(width (GoB f)))) `1 <= r & r <= ((GoB f) * (((i2 + 1) + 1),(width (GoB f)))) `1 ) }

proof

((GoB f) * ((i2 + 1),(width (GoB f)))) `1 < ((GoB f) * (((i2 + 1) + 1),(width (GoB f)))) `1 by A132, A130, A182, A198, GOBOARD5:3;
hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i2 + 1),(width (GoB f)))) `1 <= r & r <= ((GoB f) * (((i2 + 1) + 1),(width (GoB f)))) `1 ) } ; :: thesis:

end;

then p in v_strip ((GoB f),(i2 + 1)) by A182, A197, GOBOARD5:8;
then p in (v_strip ((GoB f),(i2 + 1))) /\ (h_strip ((GoB f),j2)) by A187, XBOOLE_0:def 4;
then A199: p in cell ((GoB f),(i2 + 1),j2) by GOBOARD5:def 3;
p in { |[r,s]| where r, s is Real : r <= ((GoB f) * (1,(width (GoB f)))) `1 } by A197;
then p in v_strip ((GoB f),i2) by A182, A197, GOBOARD5:10;
then p in (v_strip ((GoB f),i2)) /\ (h_strip ((GoB f),j2)) by A187, XBOOLE_0:def 4;
then p in cell ((GoB f),i2,j2) by GOBOARD5:def 3;
hence ( p in (cell ((GoB f),(i2 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) by A188, A199, XBOOLE_0:def 4; :: thesis:

end;

case A200: ( i2 + 1 = len (GoB f) & i2 > 0 ) ; :: thesis:

then A201: 0 + 1 <= i2 by NAT_1:13;
A202: p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i2,(width (GoB f)))) `1 <= r & r <= ((GoB f) * ((i2 + 1),(width (GoB f)))) `1 ) }

proof

((GoB f) * (i2,(width (GoB f)))) `1 <= ((GoB f) * ((i2 + 1),(width (GoB f)))) `1 by A128, A182, A200, A201, GOBOARD5:3;
hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i2,(width (GoB f)))) `1 <= r & r <= ((GoB f) * ((i2 + 1),(width (GoB f)))) `1 ) } ; :: thesis:

end;

p in { |[r,s]| where r, s is Real : ((GoB f) * ((len (GoB f)),(width (GoB f)))) `1 <= r } by A200;
then p in v_strip ((GoB f),(i2 + 1)) by A182, A200, GOBOARD5:9;
then p in (v_strip ((GoB f),(i2 + 1))) /\ (h_strip ((GoB f),j2)) by A187, XBOOLE_0:def 4;
then A203: p in cell ((GoB f),(i2 + 1),j2) by GOBOARD5:def 3;
i2 < len (GoB f) by A200, NAT_1:13;
then p in v_strip ((GoB f),i2) by A182, A201, A202, GOBOARD5:8;
then p in (v_strip ((GoB f),i2)) /\ (h_strip ((GoB f),j2)) by A187, XBOOLE_0:def 4;
then p in cell ((GoB f),i2,j2) by GOBOARD5:def 3;
hence ( p in (cell ((GoB f),(i2 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) by A188, A203, XBOOLE_0:def 4; :: thesis:

end;

case ( i2 + 1 = len (GoB f) & i2 = 0 ) ; :: thesis:

hence contradiction by GOBOARD7:32; :: thesis:

end;

end;

case A211: ( j2 <> 0 & j2 <> width (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 + 1),j2)),((GoB f) * ((i2 + 1),(j2 + 1)))) ) ) ) ; :: thesis:

then A212: j2 < width (GoB f) by A4, XXREAL_0:1;
then A213: j2 + 1 <= width (GoB f) by NAT_1:13;
for k being Nat st 1 <= k & k + 1 <= len f holds
LSeg (((GoB f) * ((i2 + 1),j2)),((GoB f) * ((i2 + 1),(j2 + 1)))) <> LSeg (f,k)

proof

let k be Nat; :: thesis:
assume A214: ( 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 + 1),j2)),((GoB f) * ((i2 + 1),(j2 + 1)))) <> LSeg (f,k) by A211, A214; :: thesis:

end;

then A215: ( 1 <= i2 + 1 & i2 + 1 <= len (GoB f) & 1 <= j2 & j2 + 1 <= width (GoB f) implies not (1 / 2) * (((GoB f) * ((i2 + 1),j2)) + ((GoB f) * ((i2 + 1),(j2 + 1)))) in L~ f ) by GOBOARD7:39;
reconsider p = (1 / 2) * (((GoB f) * ((i2 + 1),j2)) + ((GoB f) * ((i2 + 1),(j2 + 1)))) as Point of (TOP-REAL 2) ;
A216: p `2 = (1 / 2) * ((((GoB f) * ((i2 + 1),j2)) + ((GoB f) * ((i2 + 1),(j2 + 1)))) `2) by TOPREAL3:4
.= (1 / 2) * ((((GoB f) * ((i2 + 1),j2)) `2) + (((GoB f) * ((i2 + 1),(j2 + 1))) `2)) by TOPREAL3:2 ;
reconsider P = {p} as Subset of (TOP-REAL 2) ;
A217: 1 < width (GoB f) by GOBOARD7:33;
Down ((RightComp f),((L~ f) `)) is closed by Lm4, CONNSP_1:33;
then A218: Cl (Down ((RightComp f),((L~ f) `))) = Down ((RightComp f),((L~ f) `)) by PRE_TOPC:22;
Down ((LeftComp f),((L~ f) `)) is closed by Lm3, CONNSP_1:33;
then A219: Cl (Down ((LeftComp f),((L~ f) `))) = Down ((LeftComp f),((L~ f) `)) by PRE_TOPC:22;
(Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) = Down (((LeftComp f) \/ (RightComp f)),((L~ f) `)) by GOBRD11:4;
then A220: Cl (Down (((LeftComp f) \/ (RightComp f)),((L~ f) `))) = (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A219, A218, PRE_TOPC:20;
A221: 1 <= i2 + 1 by NAT_1:11;
p `1 = (1 / 2) * ((((GoB f) * ((i2 + 1),j2)) + ((GoB f) * ((i2 + 1),(j2 + 1)))) `1) by TOPREAL3:4
.= (1 / 2) * ((((GoB f) * ((i2 + 1),j2)) `1) + (((GoB f) * ((i2 + 1),(j2 + 1))) `1)) by TOPREAL3:2 ;
then A222: p = |[((1 / 2) * ((((GoB f) * ((i2 + 1),j2)) `1) + (((GoB f) * ((i2 + 1),(j2 + 1))) `1))),((1 / 2) * ((((GoB f) * ((i2 + 1),j2)) `2) + (((GoB f) * ((i2 + 1),(j2 + 1))) `2)))]| by A216, EUCLID:53;
A223: ( Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `)) c= Cl (Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `))) & Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `)) = Int (cell ((GoB f),i2,j2)) ) by A3, A4, Th3, PRE_TOPC:18;
A224: ( Down ((LeftComp f),((L~ f) `)) = LeftComp f & Down ((RightComp f),((L~ f) `)) = RightComp f ) by Th5;
Down ((Int (cell ((GoB f),i1,j2))),((L~ f) `)) c= (LeftComp f) \/ (RightComp f) by A1, A2, A6, A7, Th3;
then Down ((Int (cell ((GoB f),i1,j2))),((L~ f) `)) c= Down (((LeftComp f) \/ (RightComp f)),((L~ f) `)) by A224, GOBRD11:4;
then A225: Cl (Down ((Int (cell ((GoB f),i1,j2))),((L~ f) `))) c= Cl (Down (((LeftComp f) \/ (RightComp f)),((L~ f) `))) by PRE_TOPC:19;
A226: 0 + 1 <= j2 by A211, NAT_1:13;
then A227: 1 < j2 + 1 by NAT_1:13;
( ( for x being object st x in P holds
not x in L~ f ) implies P misses L~ f ) by XBOOLE_0:3;
then A228: ( p in {p} & {p} c= (L~ f) ` ) by A1, A126, A226, A212, A215, NAT_1:13, SUBSET_1:23, TARSKI:def 1;
then reconsider p1 = p as Point of ((TOP-REAL 2) | ((L~ f) `)) by PRE_TOPC:8;
A229: 1 <= 1 + i2 by NAT_1:11;
j2 < j2 + 1 by NAT_1:13;
then A230: ((GoB f) * ((i2 + 1),j2)) `2 < ((GoB f) * ((i2 + 1),(j2 + 1))) `2 by A1, A126, A226, A213, A229, GOBOARD5:4;
then (((GoB f) * ((i2 + 1),j2)) `2) + (((GoB f) * ((i2 + 1),(j2 + 1))) `2) < (((GoB f) * ((i2 + 1),(j2 + 1))) `2) + (((GoB f) * ((i2 + 1),(j2 + 1))) `2) by XREAL_1:8;
then A231: ((((GoB f) * ((i2 + 1),j2)) `2) + (((GoB f) * ((i2 + 1),(j2 + 1))) `2)) / 2 < ((((GoB f) * ((i2 + 1),(j2 + 1))) `2) + (((GoB f) * ((i2 + 1),(j2 + 1))) `2)) / 2 by XREAL_1:74;
(((GoB f) * ((i2 + 1),j2)) `2) + (((GoB f) * ((i2 + 1),j2)) `2) < (((GoB f) * ((i2 + 1),j2)) `2) + (((GoB f) * ((i2 + 1),(j2 + 1))) `2) by A230, XREAL_1:8;
then A232: ((((GoB f) * ((i2 + 1),j2)) `2) + (((GoB f) * ((i2 + 1),j2)) `2)) / 2 < ((((GoB f) * ((i2 + 1),j2)) `2) + (((GoB f) * ((i2 + 1),(j2 + 1))) `2)) / 2 by XREAL_1:74;
p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i2 + 1),j2)) `2 <= s & s <= ((GoB f) * ((i2 + 1),(j2 + 1))) `2 ) }

proof

p = |[(p `1),(p `2)]| by EUCLID:53;
hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i2 + 1),j2)) `2 <= s & s <= ((GoB f) * ((i2 + 1),(j2 + 1))) `2 ) } by A216, A232, A231; :: thesis:

end;

then A233: p in h_strip ((GoB f),j2) by A1, A126, A226, A212, A221, GOBOARD5:5;
A234: ( i2 = 0 or i2 >= 0 + 1 ) by NAT_1:13;

A235: now :: thesis:

per cases by A1, A126, A234, XXREAL_0:1;

case A236: ( i2 >= 1 & i2 + 1 < len (GoB f) ) ; :: thesis:

then A237: (i2 + 1) + 1 <= len (GoB f) by NAT_1:13;
A238: p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i2 + 1),1)) `1 <= r & r <= ((GoB f) * (((i2 + 1) + 1),1)) `1 ) }

proof

i2 + 1 < (i2 + 1) + 1 by NAT_1:13;
then A239: ((GoB f) * ((i2 + 1),1)) `1 < ((GoB f) * (((i2 + 1) + 1),1)) `1 by A217, A229, A237, GOBOARD5:3;
( ((GoB f) * ((i2 + 1),j2)) `1 = ((GoB f) * ((i2 + 1),1)) `1 & ((GoB f) * ((i2 + 1),(j2 + 1))) `1 = ((GoB f) * ((i2 + 1),1)) `1 ) by A1, A4, A126, A226, A213, A229, A227, GOBOARD5:2;
hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i2 + 1),1)) `1 <= r & r <= ((GoB f) * (((i2 + 1) + 1),1)) `1 ) } by A222, A239; :: thesis:

end;

1 <= i2 + 1 by NAT_1:11;
then p in v_strip ((GoB f),(i2 + 1)) by A217, A236, A238, GOBOARD5:8;
then p in (v_strip ((GoB f),(i2 + 1))) /\ (h_strip ((GoB f),j2)) by A233, XBOOLE_0:def 4;
then A240: p in cell ((GoB f),(i2 + 1),j2) by GOBOARD5:def 3;
A241: p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i2,1)) `1 <= r & r <= ((GoB f) * ((i2 + 1),1)) `1 ) }

proof

i2 < i2 + 1 by NAT_1:13;
then A242: ((GoB f) * (i2,1)) `1 < ((GoB f) * ((i2 + 1),1)) `1 by A217, A236, GOBOARD5:3;
( ((GoB f) * ((i2 + 1),j2)) `1 = ((GoB f) * ((i2 + 1),1)) `1 & ((GoB f) * ((i2 + 1),(j2 + 1))) `1 = ((GoB f) * ((i2 + 1),1)) `1 ) by A1, A4, A126, A226, A213, A229, A227, GOBOARD5:2;
hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i2,1)) `1 <= r & r <= ((GoB f) * ((i2 + 1),1)) `1 ) } by A222, A242; :: thesis:

end;

i2 < len (GoB f) by A236, NAT_1:13;
then p in v_strip ((GoB f),i2) by A217, A236, A241, GOBOARD5:8;
then p in (v_strip ((GoB f),i2)) /\ (h_strip ((GoB f),j2)) by A233, XBOOLE_0:def 4;
then p in cell ((GoB f),i2,j2) by GOBOARD5:def 3;
hence ( p in (cell ((GoB f),(i2 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) by A228, A240, XBOOLE_0:def 4; :: thesis:

end;

case A243: ( i2 >= 1 & i2 + 1 = len (GoB f) ) ; :: thesis:

A244: i2 < i2 + 1 by NAT_1:13;
p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i2,1)) `1 <= r & r <= ((GoB f) * ((i2 + 1),1)) `1 ) }

proof

A245: ((GoB f) * (i2,1)) `1 < ((GoB f) * ((i2 + 1),1)) `1 by A217, A243, A244, GOBOARD5:3;
( ((GoB f) * ((i2 + 1),j2)) `1 = ((GoB f) * ((i2 + 1),1)) `1 & ((GoB f) * ((i2 + 1),(j2 + 1))) `1 = ((GoB f) * ((i2 + 1),1)) `1 ) by A1, A4, A126, A226, A213, A229, A227, GOBOARD5:2;
hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * (i2,1)) `1 <= r & r <= ((GoB f) * ((i2 + 1),1)) `1 ) } by A222, A245; :: thesis:

end;

then p in v_strip ((GoB f),i2) by A217, A243, A244, GOBOARD5:8;
then p in (v_strip ((GoB f),i2)) /\ (h_strip ((GoB f),j2)) by A233, XBOOLE_0:def 4;
then A246: p in cell ((GoB f),i2,j2) by GOBOARD5:def 3;
p in { |[r,s]| where r, s is Real : ((GoB f) * ((i2 + 1),1)) `1 <= r }

proof

( ((GoB f) * ((i2 + 1),j2)) `1 = ((GoB f) * ((i2 + 1),1)) `1 & ((GoB f) * ((i2 + 1),(j2 + 1))) `1 = ((GoB f) * ((i2 + 1),1)) `1 ) by A1, A4, A126, A226, A213, A229, A227, GOBOARD5:2;
hence p in { |[r,s]| where r, s is Real : ((GoB f) * ((i2 + 1),1)) `1 <= r } by A222; :: thesis:

end;

then p in v_strip ((GoB f),(i2 + 1)) by A217, A243, GOBOARD5:9;
then p in (v_strip ((GoB f),(i2 + 1))) /\ (h_strip ((GoB f),j2)) by A233, XBOOLE_0:def 4;
then p in cell ((GoB f),(i2 + 1),j2) by GOBOARD5:def 3;
hence ( p in (cell ((GoB f),(i2 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) by A228, A246, XBOOLE_0:def 4; :: thesis:

end;

case A247: ( i2 = 0 & i2 + 1 < len (GoB f) ) ; :: thesis:

then A248: (i2 + 1) + 1 <= len (GoB f) by NAT_1:13;
p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i2 + 1),1)) `1 <= r & r <= ((GoB f) * (((i2 + 1) + 1),1)) `1 ) }

proof

i2 + 1 < (i2 + 1) + 1 by NAT_1:13;
then A249: ((GoB f) * ((i2 + 1),1)) `1 < ((GoB f) * (((i2 + 1) + 1),1)) `1 by A217, A229, A248, GOBOARD5:3;
( ((GoB f) * ((i2 + 1),j2)) `1 = ((GoB f) * ((i2 + 1),1)) `1 & ((GoB f) * ((i2 + 1),(j2 + 1))) `1 = ((GoB f) * ((i2 + 1),1)) `1 ) by A1, A4, A126, A226, A213, A229, A227, GOBOARD5:2;
hence p in { |[r,s]| where r, s is Real : ( ((GoB f) * ((i2 + 1),1)) `1 <= r & r <= ((GoB f) * (((i2 + 1) + 1),1)) `1 ) } by A222, A249; :: thesis:

end;

then p in v_strip ((GoB f),i1) by A126, A217, A247, GOBOARD5:8;
then p in (v_strip ((GoB f),(i2 + 1))) /\ (h_strip ((GoB f),j2)) by A126, A233, XBOOLE_0:def 4;
then A250: p in cell ((GoB f),(i2 + 1),j2) by GOBOARD5:def 3;
p in { |[r,s]| where r, s is Real : r <= ((GoB f) * (1,1)) `1 }

proof

( ((GoB f) * ((i2 + 1),j2)) `1 = ((GoB f) * ((i2 + 1),1)) `1 & ((GoB f) * ((i2 + 1),(j2 + 1))) `1 = ((GoB f) * ((i2 + 1),1)) `1 ) by A1, A4, A126, A226, A213, A229, A227, GOBOARD5:2;
hence p in { |[r,s]| where r, s is Real : r <= ((GoB f) * (1,1)) `1 } by A222, A247; :: thesis:

end;

then p in v_strip ((GoB f),i2) by A217, A247, GOBOARD5:10;
then p in (v_strip ((GoB f),i2)) /\ (h_strip ((GoB f),j2)) by A233, XBOOLE_0:def 4;
then p in cell ((GoB f),i2,j2) by GOBOARD5:def 3;
hence ( p in (cell ((GoB f),(i2 + 1),j2)) /\ ((L~ f) `) & p in (cell ((GoB f),i2,j2)) /\ ((L~ f) `) ) by A228, A250, XBOOLE_0:def 4; :: thesis:

end;

case ( i2 = 0 & i2 + 1 = len (GoB f) ) ; :: thesis:

hence contradiction by GOBOARD7:32; :: thesis:

end;

then p in Cl (Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `))) by A3, A4, Th2;
then A251: Cl (Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `))) c= Component_of p1 by A3, A4, Th3, GOBRD11:1;
p in Cl (Down ((Int (cell ((GoB f),i1,j2))),((L~ f) `))) by A4, A126, A235, Th2;
then Component_of p1 c= (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A225, A220, Th5, CONNSP_3:21;
then Cl (Down ((Int (cell ((GoB f),i2,j2))),((L~ f) `))) c= (Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) by A251;
hence Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) by A224, A223; :: 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: