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

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

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

end;

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