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