let f be non constant standard special_circular_sequence; :: thesis:
let i1, j1, i2, j2 be Element of NAT ; :: thesis:
assume A1: ( i1 <= len (GoB f) & j1 <= width (GoB f) & i2 <= len (GoB f) & j2 <= width (GoB f) & ( j2 = j1 + 1 or j1 = j2 + 1 ) & i1 = i2 ) ; :: thesis:

assume A2: Int (cell (GoB f),i1,j1) c= (LeftComp f) \/ (RightComp f) ; :: thesis:

per cases by A1;

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

per cases ;

case ex k being Element of NAT st
( 1 <= k & k + 1 <= len f & i2 <> 0 & i2 <> len (GoB f) & LSeg (f /. k),(f /. (k + 1)) = LSeg ((GoB f) * i2,(j1 + 1)),((GoB f) * (i2 + 1),(j1 + 1)) ) ; :: thesis:

then consider k being Element of NAT such that
A4: ( 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)) ) ;

per cases by A4, SPPOL_1:25;

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

A6: Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] by MATRIX_1:def 5;
0 + 1 <= j1 + 1 by XREAL_1:8;
then A7: j1 + 1 in Seg (width (GoB f)) by A1, A3, FINSEQ_1:3;
i2 > 0 by A4;
then i2 >= 0 + 1 by NAT_1:13;
then i2 in dom (GoB f) by A1, FINSEQ_3:27;
then A8: [i2,(j1 + 1)] in Indices (GoB f) by A6, A7, ZFMISC_1:106;
i2 < len (GoB f) by A1, A4, XXREAL_0:1;
then A9: i2 + 1 <= len (GoB f) by NAT_1:13;
1 <= i2 + 1 by NAT_1:11;
then i2 + 1 in dom (GoB f) by A9, FINSEQ_3:27;
then [(i2 + 1),(j1 + 1)] in Indices (GoB f) by A6, A7, ZFMISC_1:106;
then A10: left_cell f,k = cell (GoB f),i2,(j1 + 1) by A4, A5, A8, GOBOARD5:29;
A11: Int (left_cell f,k) c= LeftComp f by A4, GOBOARD9:24;
LeftComp f c= (LeftComp f) \/ (RightComp f) by XBOOLE_1:7;
hence Int (cell (GoB f),i2,(j1 + 1)) c= (LeftComp f) \/ (RightComp f) by A10, A11, XBOOLE_1:1; :: thesis:

end;

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

A13: Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] by MATRIX_1:def 5;
0 + 1 <= j1 + 1 by XREAL_1:8;
then A14: j1 + 1 in Seg (width (GoB f)) by A1, A3, FINSEQ_1:3;
i2 > 0 by A4;
then i2 >= 0 + 1 by NAT_1:13;
then i2 in dom (GoB f) by A1, FINSEQ_3:27;
then A15: [i2,(j1 + 1)] in Indices (GoB f) by A13, A14, ZFMISC_1:106;
i2 < len (GoB f) by A1, A4, XXREAL_0:1;
then A16: i2 + 1 <= len (GoB f) by NAT_1:13;
1 <= i2 + 1 by NAT_1:11;
then i2 + 1 in dom (GoB f) by A16, FINSEQ_3:27;
then [(i2 + 1),(j1 + 1)] in Indices (GoB f) by A13, A14, ZFMISC_1:106;
then A17: right_cell f,k = cell (GoB f),i2,(j1 + 1) by A4, A12, A15, GOBOARD5:30;
A18: Int (right_cell f,k) c= RightComp f by A4, GOBOARD9:28;
RightComp f c= (LeftComp f) \/ (RightComp f) by XBOOLE_1:7;
hence Int (cell (GoB f),i2,(j1 + 1)) c= (LeftComp f) \/ (RightComp f) by A17, A18, XBOOLE_1:1; :: thesis:

end;

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

end;

case A19: for k being Element of NAT holds
( not 1 <= k or not k + 1 <= len f or not i2 <> 0 or not i2 <> len (GoB f) or not LSeg (f /. k),(f /. (k + 1)) = LSeg ((GoB f) * i2,(j1 + 1)),((GoB f) * (i2 + 1),(j1 + 1)) ) ; :: thesis:

per cases by A19;

case A20: i2 = 0 ; :: thesis:

reconsider p = |[((((GoB f) * 1,(j1 + 1)) `1 ) - 1),(((GoB f) * 1,(j1 + 1)) `2 )]| as Point of (TOP-REAL 2) ;
A21: 1 < len (GoB f) by GOBOARD7:34;
A22: 1 < width (GoB f) by GOBOARD7:35;
A23: 1 <= 1 + j1 by NAT_1:11;
then ((GoB f) * 1,(j1 + 1)) `1 = ((GoB f) * 1,1) `1 by A1, A3, A21, GOBOARD5:3;
then A24: p `1 = (((GoB f) * 1,1) `1 ) - 1 by EUCLID:56;
A25: p `1 < (p `1 ) + 1 by XREAL_1:31;
A26: p in {p} by TARSKI:def 1;
reconsider P = {p} as Subset of (TOP-REAL 2) ;
( ( 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 A27: {p} c= (L~ f) ` by A24, A25, SUBSET_1:43, TARSKI:def 1;
then reconsider p1 = p as Point of ((TOP-REAL 2) | ((L~ f) ` )) by A26, PRE_TOPC:29;
p in { |[s,r]| where s, r is Real : s <= ((GoB f) * 1,1) `1 }