let f be non constant standard special_circular_sequence; :: thesis: LSeg (((GoB f) * 1,1) - |[1,1]|),(((1 / 2) * (((GoB f) * 1,1) + ((GoB f) * 2,1))) - |[0 ,1]|) misses L~ f
A1: 1 <= width (GoB f) by GOBOARD7:35;

now

let p be Point of (TOP-REAL 2); :: thesis: ( p in LSeg (((GoB f) * 1,1) - |[1,1]|),(((1 / 2) * (((GoB f) * 1,1) + ((GoB f) * 2,1))) - |[0 ,1]|) implies p `2 < ((GoB f) * 1,1) `2 )
assume A2: p in LSeg (((GoB f) * 1,1) - |[1,1]|),(((1 / 2) * (((GoB f) * 1,1) + ((GoB f) * 2,1))) - |[0 ,1]|) ; :: thesis: p `2 < ((GoB f) * 1,1) `2
1 < len (GoB f) by GOBOARD7:34;
then 1 + 1 <= len (GoB f) by NAT_1:13;
then A3: ((GoB f) * 2,1) `2 = ((GoB f) * 1,1) `2 by A1, GOBOARD5:2;
(((GoB f) * 1,1) - |[1,1]|) `2 = (((GoB f) * 1,1) `2 ) - (|[1,1]| `2 ) by TOPREAL3:8
.= (((GoB f) * 1,1) `2 ) - 1 by EUCLID:56 ;
then A4: ((GoB f) * 1,1) - |[1,1]| = |[((((GoB f) * 1,1) - |[1,1]|) `1 ),((((GoB f) * 1,1) `2 ) - 1)]| by EUCLID:57;
(((1 / 2) * (((GoB f) * 1,1) + ((GoB f) * 2,1))) - |[0 ,1]|) `2 = (((1 / 2) * (((GoB f) * 1,1) + ((GoB f) * 2,1))) `2 ) - (|[0 ,1]| `2 ) by TOPREAL3:8
.= ((1 / 2) * ((((GoB f) * 1,1) + ((GoB f) * 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 A3, TOPREAL3:7
.= (1 * (((GoB f) * 1,1) `2 )) - 1 by EUCLID:56 ;
then ((1 / 2) * (((GoB f) * 1,1) + ((GoB f) * 2,1))) - |[0 ,1]| = |[((((1 / 2) * (((GoB f) * 1,1) + ((GoB f) * 2,1))) - |[0 ,1]|) `1 ),((((GoB f) * 1,1) `2 ) - 1)]| by EUCLID:57;
then p `2 = (((GoB f) * 1,1) `2 ) - 1 by A2, A4, TOPREAL3:18;
hence p `2 < ((GoB f) * 1,1) `2 by XREAL_1:46; :: thesis: verum

end;

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