let f be non constant standard special_circular_sequence; LSeg ((((GoB f) * (1,1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (1,2)))) - |[1,0]|)) misses L~ f
A1:
1 <= len (GoB f)
by GOBOARD7:32;
now for p being Point of (TOP-REAL 2) st p in LSeg ((((GoB f) * (1,1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (1,2)))) - |[1,0]|)) holds
p `1 < ((GoB f) * (1,1)) `1
1
< width (GoB f)
by GOBOARD7:33;
then
1
+ 1
<= width (GoB f)
by NAT_1:13;
then A2:
((GoB f) * (1,2)) `1 = ((GoB f) * (1,1)) `1
by A1, GOBOARD5:2;
(((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (1,2)))) - |[1,0]|) `1 =
(((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (1,2)))) `1) - (|[1,0]| `1)
by TOPREAL3:3
.=
((1 / 2) * ((((GoB f) * (1,1)) + ((GoB f) * (1,2))) `1)) - (|[1,0]| `1)
by TOPREAL3:4
.=
((1 / 2) * ((((GoB f) * (1,1)) `1) + (((GoB f) * (1,1)) `1))) - (|[1,0]| `1)
by A2, TOPREAL3:2
.=
(1 * (((GoB f) * (1,1)) `1)) - 1
by EUCLID:52
;
then A3:
((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (1,2)))) - |[1,0]| = |[((((GoB f) * (1,1)) `1) - 1),((((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (1,2)))) - |[1,0]|) `2)]|
by EUCLID:53;
(((GoB f) * (1,1)) - |[1,1]|) `1 =
(((GoB f) * (1,1)) `1) - (|[1,1]| `1)
by TOPREAL3:3
.=
(((GoB f) * (1,1)) `1) - 1
by EUCLID:52
;
then A4:
((GoB f) * (1,1)) - |[1,1]| = |[((((GoB f) * (1,1)) `1) - 1),((((GoB f) * (1,1)) - |[1,1]|) `2)]|
by EUCLID:53;
let p be
Point of
(TOP-REAL 2);
( p in LSeg ((((GoB f) * (1,1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (1,2)))) - |[1,0]|)) implies p `1 < ((GoB f) * (1,1)) `1 )assume
p in LSeg (
(((GoB f) * (1,1)) - |[1,1]|),
(((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (1,2)))) - |[1,0]|))
;
p `1 < ((GoB f) * (1,1)) `1 then
p `1 = (((GoB f) * (1,1)) `1) - 1
by A4, A3, TOPREAL3:11;
hence
p `1 < ((GoB f) * (1,1)) `1
by XREAL_1:44;
verum end;
hence
LSeg ((((GoB f) * (1,1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (1,2)))) - |[1,0]|)) misses L~ f
by Th21; verum