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

now :: thesis: for p being Point of (TOP-REAL 2) st p in LSeg ((((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1)))) - |[0,1]|),(((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|)) holds
p `2 < ((GoB f) * (1,1)) `2

A2: 1 < len (GoB f) by GOBOARD7:32;
then A3: ((len (GoB f)) -' 1) + 1 = len (GoB f) by XREAL_1:235;
then A4: (len (GoB f)) -' 1 <= len (GoB f) by NAT_1:11;
A5: ((GoB f) * ((len (GoB f)),1)) `2 = ((GoB f) * (1,1)) `2 by A1, A2, GOBOARD5:1;
then (((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|) `2 = (((GoB f) * (1,1)) `2) + (|[1,(- 1)]| `2) by TOPREAL3:2
.= (((GoB f) * (1,1)) `2) + (- 1) by EUCLID:52
.= (((GoB f) * (1,1)) `2) - 1 ;
then A6: ((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]| = |[((((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|) `1),((((GoB f) * (1,1)) `2) - 1)]| by EUCLID:53;
1 <= (len (GoB f)) -' 1 by A2, A3, NAT_1:13;
then A7: ((GoB f) * (((len (GoB f)) -' 1),1)) `2 = ((GoB f) * (1,1)) `2 by A1, A4, GOBOARD5:1;
(((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1)))) - |[0,1]|) `2 = (((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1)))) `2) - (|[0,1]| `2) by TOPREAL3:3
.= ((1 / 2) * ((((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1))) `2)) - (|[0,1]| `2) by TOPREAL3:4
.= ((1 / 2) * ((((GoB f) * (1,1)) `2) + (((GoB f) * (1,1)) `2))) - (|[0,1]| `2) by A7, A5, TOPREAL3:2
.= (1 * (((GoB f) * (1,1)) `2)) - 1 by EUCLID:52 ;
then A8: ((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1)))) - |[0,1]| = |[((((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1)))) - |[0,1]|) `1),((((GoB f) * (1,1)) `2) - 1)]| by EUCLID:53;
let p be Point of (TOP-REAL 2); :: thesis: ( p in LSeg ((((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1)))) - |[0,1]|),(((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|)) implies p `2 < ((GoB f) * (1,1)) `2 )
assume p in LSeg ((((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1)))) - |[0,1]|),(((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|)) ; :: thesis: p `2 < ((GoB f) * (1,1)) `2
then p `2 = (((GoB f) * (1,1)) `2) - 1 by A8, A6, TOPREAL3:12;
hence p `2 < ((GoB f) * (1,1)) `2 by XREAL_1:44; :: thesis: verum

end;

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