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