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

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

per cases by A1;

case A3: i2 = i1 + 1 ; :: thesis:

per cases ;

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

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

per cases by A4, SPPOL_1:25;

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

A6: Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] by MATRIX_1:def 5;
0 + 1 <= i1 + 1 by XREAL_1:8;
then A7: i1 + 1 in dom (GoB f) by A1, A3, FINSEQ_3:27;
j2 > 0 by A4;
then j2 >= 0 + 1 by NAT_1:13;
then j2 in Seg (width (GoB f)) by A1, FINSEQ_1:3;
then A8: [(i1 + 1),j2] in Indices (GoB f) by A6, A7, ZFMISC_1:106;
j2 < width (GoB f) by A1, A4, XXREAL_0:1;
then A9: j2 + 1 <= width (GoB f) by NAT_1:13;
1 <= j2 + 1 by NAT_1:11;
then j2 + 1 in Seg (width (GoB f)) by A9, FINSEQ_1:3;
then [(i1 + 1),(j2 + 1)] in Indices (GoB f) by A6, A7, ZFMISC_1:106;
then A10: right_cell f,k = cell (GoB f),(i1 + 1),j2 by A4, A5, A8, GOBOARD5:28;
A11: 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),(i1 + 1),j2) c= (LeftComp f) \/ (RightComp f) by A10, A11, XBOOLE_1:1; :: thesis:

end;

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

A13: Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] by MATRIX_1:def 5;
0 + 1 <= i1 + 1 by XREAL_1:8;
then A14: i1 + 1 in dom (GoB f) by A1, A3, FINSEQ_3:27;
j2 > 0 by A4;
then j2 >= 0 + 1 by NAT_1:13;
then j2 in Seg (width (GoB f)) by A1, FINSEQ_1:3;
then A15: [(i1 + 1),j2] in Indices (GoB f) by A13, A14, ZFMISC_1:106;
j2 < width (GoB f) by A1, A4, XXREAL_0:1;
then A16: j2 + 1 <= width (GoB f) by NAT_1:13;
1 <= j2 + 1 by NAT_1:11;
then j2 + 1 in Seg (width (GoB f)) by A16, FINSEQ_1:3;
then [(i1 + 1),(j2 + 1)] in Indices (GoB f) by A13, A14, ZFMISC_1:106;
then A17: left_cell f,k = cell (GoB f),(i1 + 1),j2 by A4, A12, A15, GOBOARD5:31;
A18: 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),(i1 + 1),j2) c= (LeftComp f) \/ (RightComp f) by A17, A18, XBOOLE_1:1; :: thesis:

end;

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

per cases by A19;

case A20: j2 = 0 ; :: thesis:

reconsider p = |[(((GoB f) * (i1 + 1),1) `1 ),((((GoB f) * (i1 + 1),1) `2 ) - 1)]| as Point of (TOP-REAL 2) ;
A21: 1 < width (GoB f) by GOBOARD7:35;
A22: 1 < len (GoB f) by GOBOARD7:34;
A23: 1 <= i1 + 1 by NAT_1:11;
then ((GoB f) * (i1 + 1),1) `2 = ((GoB f) * 1,1) `2 by A1, A3, A21, GOBOARD5:2;
then A24: p `2 = (((GoB f) * 1,1) `2 ) - 1 by EUCLID:56;
A25: p `2 < (p `2 ) + 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 `2 < ((GoB f) * 1,1) `2 ) implies P misses L~ f ) by GOBOARD8:23;
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 { |[r,s]| where r, s is Real : s <= ((GoB f) * 1,1) `2 }