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