let f be non constant standard special_circular_sequence; :: thesis: for i being Nat st 1 <= i & i + 2 <= len (GoB f) holds
LSeg ((((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|),(((1 / 2) * (((GoB f) * ((i + 1),(width (GoB f)))) + ((GoB f) * ((i + 2),(width (GoB f)))))) + |[0,1]|)) misses L~ f
let i be Nat; :: thesis: ( 1 <= i & i + 2 <= len (GoB f) implies LSeg ((((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|),(((1 / 2) * (((GoB f) * ((i + 1),(width (GoB f)))) + ((GoB f) * ((i + 2),(width (GoB f)))))) + |[0,1]|)) misses L~ f )
assume that
A1: 1 <= i and
A2: i + 2 <= len (GoB f) ; :: thesis: LSeg ((((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|),(((1 / 2) * (((GoB f) * ((i + 1),(width (GoB f)))) + ((GoB f) * ((i + 2),(width (GoB f)))))) + |[0,1]|)) misses L~ f
A3: 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) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|),(((1 / 2) * (((GoB f) * ((i + 1),(width (GoB f)))) + ((GoB f) * ((i + 2),(width (GoB f)))))) + |[0,1]|)) holds
p `2 > ((GoB f) * (1,(width (GoB f)))) `2
A4: i <= i + 2 by NAT_1:11;
then i <= len (GoB f) by A2, XXREAL_0:2;
then A5: ((GoB f) * (i,(width (GoB f)))) `2 = ((GoB f) * (1,(width (GoB f)))) `2 by A1, A3, GOBOARD5:1;
i + 1 <= i + 2 by XREAL_1:6;
then ( 1 <= i + 1 & i + 1 <= len (GoB f) ) by A2, NAT_1:11, XXREAL_0:2;
then A6: ((GoB f) * ((i + 1),(width (GoB f)))) `2 = ((GoB f) * (1,(width (GoB f)))) `2 by A3, GOBOARD5:1;
1 <= i + 2 by A1, A4, XXREAL_0:2;
then A7: ((GoB f) * ((i + 2),(width (GoB f)))) `2 = ((GoB f) * (1,(width (GoB f)))) `2 by A2, A3, GOBOARD5:1;
(((1 / 2) * (((GoB f) * ((i + 1),(width (GoB f)))) + ((GoB f) * ((i + 2),(width (GoB f)))))) + |[0,1]|) `2 = (((1 / 2) * (((GoB f) * ((i + 1),(width (GoB f)))) + ((GoB f) * ((i + 2),(width (GoB f)))))) `2) + (|[0,1]| `2) by TOPREAL3:2
.= ((1 / 2) * ((((GoB f) * ((i + 1),(width (GoB f)))) + ((GoB f) * ((i + 2),(width (GoB f))))) `2)) + (|[0,1]| `2) by TOPREAL3:4
.= ((1 / 2) * ((((GoB f) * (1,(width (GoB f)))) `2) + (((GoB f) * (1,(width (GoB f)))) `2))) + (|[0,1]| `2) by A6, A7, TOPREAL3:2
.= (1 * (((GoB f) * (1,(width (GoB f)))) `2)) + 1 by EUCLID:52 ;
then A8: ((1 / 2) * (((GoB f) * ((i + 1),(width (GoB f)))) + ((GoB f) * ((i + 2),(width (GoB f)))))) + |[0,1]| = |[((((1 / 2) * (((GoB f) * ((i + 1),(width (GoB f)))) + ((GoB f) * ((i + 2),(width (GoB f)))))) + |[0,1]|) `1),((((GoB f) * (1,(width (GoB f)))) `2) + 1)]| by EUCLID:53;
(((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|) `2 = (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `2) + (|[0,1]| `2) by TOPREAL3:2
.= ((1 / 2) * ((((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) `2)) + (|[0,1]| `2) by TOPREAL3:4
.= ((1 / 2) * ((((GoB f) * (1,(width (GoB f)))) `2) + (((GoB f) * (1,(width (GoB f)))) `2))) + (|[0,1]| `2) by A5, A6, TOPREAL3:2
.= (1 * (((GoB f) * (1,(width (GoB f)))) `2)) + 1 by EUCLID:52 ;
then A9: ((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]| = |[((((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|) `1),((((GoB f) * (1,(width (GoB f)))) `2) + 1)]| by EUCLID:53;
let p be Point of (TOP-REAL 2); :: thesis: ( p in LSeg ((((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|),(((1 / 2) * (((GoB f) * ((i + 1),(width (GoB f)))) + ((GoB f) * ((i + 2),(width (GoB f)))))) + |[0,1]|)) implies p `2 > ((GoB f) * (1,(width (GoB f)))) `2 )
assume p in LSeg ((((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|),(((1 / 2) * (((GoB f) * ((i + 1),(width (GoB f)))) + ((GoB f) * ((i + 2),(width (GoB f)))))) + |[0,1]|)) ; :: thesis: p `2 > ((GoB f) * (1,(width (GoB f)))) `2
then p `2 = (((GoB f) * (1,(width (GoB f)))) `2) + 1 by A9, A8, TOPREAL3:12;
hence p `2 > ((GoB f) * (1,(width (GoB f)))) `2 by XREAL_1:29; :: thesis: verum
end;
hence LSeg ((((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|),(((1 / 2) * (((GoB f) * ((i + 1),(width (GoB f)))) + ((GoB f) * ((i + 2),(width (GoB f)))))) + |[0,1]|)) misses L~ f by Th24; :: thesis: verum