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

now

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

end;

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