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

now

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

end;

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