let i, j be Element of NAT ; :: thesis:
let f be non constant standard special_circular_sequence; :: thesis:
set mi = (1 / 2) * (((GoB f) * i,j) + ((GoB f) * (i + 1),j));
assume that
A1: ( 1 <= i & i + 1 <= len (GoB f) ) and
A2: ( 1 <= j & j <= width (GoB f) ) and
A3: (1 / 2) * (((GoB f) * i,j) + ((GoB f) * (i + 1),j)) in L~ f ; :: thesis:
L~ f = union { (LSeg f,k) where k is Element of NAT : ( 1 <= k & k + 1 <= len f ) } by TOPREAL1:def 6;
then consider x being set such that
A4: (1 / 2) * (((GoB f) * i,j) + ((GoB f) * (i + 1),j)) in x and
A5: x in { (LSeg f,k) where k is Element of NAT : ( 1 <= k & k + 1 <= len f ) } by A3, TARSKI:def 4;
consider k being Element of NAT such that
A6: x = LSeg f,k and
A7: ( 1 <= k & k + 1 <= len f ) by A5;
take k ; :: thesis:
thus ( 1 <= k & k + 1 <= len f ) by A7; :: thesis:
A8: f is_sequence_on GoB f by GOBOARD5:def 5;
k <= k + 1 by NAT_1:11;
then k <= len f by A7, XXREAL_0:2;
then A9: k in dom f by A7, FINSEQ_3:27;
then consider i1, j1 being Element of NAT such that
A10: [i1,j1] in Indices (GoB f) and
A11: f /. k = (GoB f) * i1,j1 by A8, GOBOARD1:def 11;
1 <= k + 1 by NAT_1:11;
then A12: k + 1 in dom f by A7, FINSEQ_3:27;
then consider i2, j2 being Element of NAT such that
A13: [i2,j2] in Indices (GoB f) and
A14: f /. (k + 1) = (GoB f) * i2,j2 by A8, GOBOARD1:def 11;
(abs (j1 - j2)) + (abs (i1 - i2)) = 1 by A8, A9, A10, A11, A12, A13, A14, GOBOARD1:def 11;
then A15: ( ( abs (j1 - j2) = 1 & i1 = i2 ) or ( abs (i1 - i2) = 1 & j1 = j2 ) ) by GOBOARD1:2;
A16: ( 1 <= j1 & j1 <= width (GoB f) ) by A10, MATRIX_1:39;
A17: ( 1 <= i1 & i1 <= len (GoB f) ) by A10, MATRIX_1:39;
A18: ( 1 <= j2 & j2 <= width (GoB f) ) by A13, MATRIX_1:39;
A19: ( 1 <= i2 & i2 <= len (GoB f) ) by A13, MATRIX_1:39;
A20: (1 / 2) * (((GoB f) * i,j) + ((GoB f) * (i + 1),j)) in LSeg (f /. k),(f /. (k + 1)) by A4, A6, A7, TOPREAL1:def 5;

per cases by A15, GOBOARD1:1;

suppose A21: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis:

then (1 / 2) * (((GoB f) * i,j) + ((GoB f) * (i + 1),j)) in LSeg ((GoB f) * i2,j2),((GoB f) * i2,(j2 + 1)) by A4, A6, A7, A11, A14, TOPREAL1:def 5;
hence LSeg ((GoB f) * i,j),((GoB f) * (i + 1),j) = LSeg f,k by A1, A2, A16, A18, A19, A21, Th29; :: thesis:

end;

suppose A22: ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis:

then (1 / 2) * (((GoB f) * i,j) + ((GoB f) * (i + 1),j)) in LSeg ((GoB f) * i1,j1),((GoB f) * i1,(j1 + 1)) by A4, A6, A7, A11, A14, TOPREAL1:def 5;
hence LSeg ((GoB f) * i,j),((GoB f) * (i + 1),j) = LSeg f,k by A1, A2, A16, A17, A18, A22, Th29; :: thesis:

end;

suppose A23: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis:

then ( j = j2 & i = i2 ) by A1, A2, A11, A14, A16, A17, A19, A20, Th28;
hence LSeg ((GoB f) * i,j),((GoB f) * (i + 1),j) = LSeg f,k by A7, A11, A14, A23, TOPREAL1:def 5; :: thesis:

end;

suppose A24: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis:

then ( j = j1 & i = i1 ) by A1, A2, A11, A14, A16, A17, A19, A20, Th28;
hence LSeg ((GoB f) * i,j),((GoB f) * (i + 1),j) = LSeg f,k by A7, A11, A14, A24, TOPREAL1:def 5; :: thesis:

end;