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

now

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

end;

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