let f be non constant standard special_circular_sequence; :: thesis: for j being Element of NAT st 1 <= j & j + 2 <= width (GoB f) holds
LSeg (((1 / 2) * (((GoB f) * 1,j) + ((GoB f) * 1,(j + 1)))) - |[1,0 ]|),(((1 / 2) * (((GoB f) * 1,(j + 1)) + ((GoB f) * 1,(j + 2)))) - |[1,0 ]|) misses L~ f
let j be Element of NAT ; :: thesis: ( 1 <= j & j + 2 <= width (GoB f) implies LSeg (((1 / 2) * (((GoB f) * 1,j) + ((GoB f) * 1,(j + 1)))) - |[1,0 ]|),(((1 / 2) * (((GoB f) * 1,(j + 1)) + ((GoB f) * 1,(j + 2)))) - |[1,0 ]|) misses L~ f )
assume that
A1: 1 <= j and
A2: j + 2 <= width (GoB f) ; :: thesis: LSeg (((1 / 2) * (((GoB f) * 1,j) + ((GoB f) * 1,(j + 1)))) - |[1,0 ]|),(((1 / 2) * (((GoB f) * 1,(j + 1)) + ((GoB f) * 1,(j + 2)))) - |[1,0 ]|) misses L~ f
A3: 1 <= len (GoB f) by GOBOARD7:34;

now

A4: j <= j + 2 by NAT_1:11;
then j <= width (GoB f) by A2, XXREAL_0:2;
then A5: ((GoB f) * 1,j) `1 = ((GoB f) * 1,1) `1 by A1, A3, GOBOARD5:3;
j + 1 <= j + 2 by XREAL_1:8;
then ( 1 <= j + 1 & j + 1 <= width (GoB f) ) by A2, NAT_1:11, XXREAL_0:2;
then A6: ((GoB f) * 1,(j + 1)) `1 = ((GoB f) * 1,1) `1 by A3, GOBOARD5:3;
1 <= j + 2 by A1, A4, XXREAL_0:2;
then A7: ((GoB f) * 1,(j + 2)) `1 = ((GoB f) * 1,1) `1 by A2, A3, GOBOARD5:3;
(((1 / 2) * (((GoB f) * 1,(j + 1)) + ((GoB f) * 1,(j + 2)))) - |[1,0 ]|) `1 = (((1 / 2) * (((GoB f) * 1,(j + 1)) + ((GoB f) * 1,(j + 2)))) `1 ) - (|[1,0 ]| `1 ) by TOPREAL3:8
.= ((1 / 2) * ((((GoB f) * 1,(j + 1)) + ((GoB f) * 1,(j + 2))) `1 )) - (|[1,0 ]| `1 ) by TOPREAL3:9
.= ((1 / 2) * ((((GoB f) * 1,1) `1 ) + (((GoB f) * 1,1) `1 ))) - (|[1,0 ]| `1 ) by A6, A7, TOPREAL3:7
.= (1 * (((GoB f) * 1,1) `1 )) - 1 by EUCLID:56 ;
then A8: ((1 / 2) * (((GoB f) * 1,(j + 1)) + ((GoB f) * 1,(j + 2)))) - |[1,0 ]| = |[((((GoB f) * 1,1) `1 ) - 1),((((1 / 2) * (((GoB f) * 1,(j + 1)) + ((GoB f) * 1,(j + 2)))) - |[1,0 ]|) `2 )]| by EUCLID:57;
(((1 / 2) * (((GoB f) * 1,j) + ((GoB f) * 1,(j + 1)))) - |[1,0 ]|) `1 = (((1 / 2) * (((GoB f) * 1,j) + ((GoB f) * 1,(j + 1)))) `1 ) - (|[1,0 ]| `1 ) by TOPREAL3:8
.= ((1 / 2) * ((((GoB f) * 1,j) + ((GoB f) * 1,(j + 1))) `1 )) - (|[1,0 ]| `1 ) by TOPREAL3:9
.= ((1 / 2) * ((((GoB f) * 1,1) `1 ) + (((GoB f) * 1,1) `1 ))) - (|[1,0 ]| `1 ) by A5, A6, TOPREAL3:7
.= (1 * (((GoB f) * 1,1) `1 )) - 1 by EUCLID:56 ;
then A9: ((1 / 2) * (((GoB f) * 1,j) + ((GoB f) * 1,(j + 1)))) - |[1,0 ]| = |[((((GoB f) * 1,1) `1 ) - 1),((((1 / 2) * (((GoB f) * 1,j) + ((GoB f) * 1,(j + 1)))) - |[1,0 ]|) `2 )]| by EUCLID:57;
let p be Point of (TOP-REAL 2); :: thesis: ( p in LSeg (((1 / 2) * (((GoB f) * 1,j) + ((GoB f) * 1,(j + 1)))) - |[1,0 ]|),(((1 / 2) * (((GoB f) * 1,(j + 1)) + ((GoB f) * 1,(j + 2)))) - |[1,0 ]|) implies p `1 < ((GoB f) * 1,1) `1 )
assume p in LSeg (((1 / 2) * (((GoB f) * 1,j) + ((GoB f) * 1,(j + 1)))) - |[1,0 ]|),(((1 / 2) * (((GoB f) * 1,(j + 1)) + ((GoB f) * 1,(j + 2)))) - |[1,0 ]|) ; :: thesis: p `1 < ((GoB f) * 1,1) `1
then p `1 = (((GoB f) * 1,1) `1 ) - 1 by A9, A8, TOPREAL3:17;
hence p `1 < ((GoB f) * 1,1) `1 by XREAL_1:46; :: thesis: verum

end;

hence LSeg (((1 / 2) * (((GoB f) * 1,j) + ((GoB f) * 1,(j + 1)))) - |[1,0 ]|),(((1 / 2) * (((GoB f) * 1,(j + 1)) + ((GoB f) * 1,(j + 2)))) - |[1,0 ]|) misses L~ f by Th21; :: thesis: verum