let f be non constant standard special_circular_sequence; for k being Element of NAT st 1 <= k & k + 2 <= len f holds
for i being Element of NAT st 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * (i + 1),1 & ( ( f /. k = (GoB f) * (i + 2),1 & f /. (k + 2) = (GoB f) * (i + 1),2 ) or ( f /. (k + 2) = (GoB f) * (i + 2),1 & f /. k = (GoB f) * (i + 1),2 ) ) holds
LSeg (((1 / 2) * (((GoB f) * i,1) + ((GoB f) * (i + 1),1))) - |[0 ,1]|),((1 / 2) * (((GoB f) * i,1) + ((GoB f) * (i + 1),2))) misses L~ f
let k be Element of NAT ; ( 1 <= k & k + 2 <= len f implies for i being Element of NAT st 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * (i + 1),1 & ( ( f /. k = (GoB f) * (i + 2),1 & f /. (k + 2) = (GoB f) * (i + 1),2 ) or ( f /. (k + 2) = (GoB f) * (i + 2),1 & f /. k = (GoB f) * (i + 1),2 ) ) holds
LSeg (((1 / 2) * (((GoB f) * i,1) + ((GoB f) * (i + 1),1))) - |[0 ,1]|),((1 / 2) * (((GoB f) * i,1) + ((GoB f) * (i + 1),2))) misses L~ f )
assume that
A1:
k >= 1
and
A2:
k + 2 <= len f
; for i being Element of NAT st 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * (i + 1),1 & ( ( f /. k = (GoB f) * (i + 2),1 & f /. (k + 2) = (GoB f) * (i + 1),2 ) or ( f /. (k + 2) = (GoB f) * (i + 2),1 & f /. k = (GoB f) * (i + 1),2 ) ) holds
LSeg (((1 / 2) * (((GoB f) * i,1) + ((GoB f) * (i + 1),1))) - |[0 ,1]|),((1 / 2) * (((GoB f) * i,1) + ((GoB f) * (i + 1),2))) misses L~ f
A3:
(k + 1) + 1 = k + (1 + 1)
;
then
k + 1 < len f
by A2, NAT_1:13;
then A4:
LSeg f,k = LSeg (f /. k),(f /. (k + 1))
by A1, TOPREAL1:def 5;
1 <= k + 1
by NAT_1:11;
then A5:
LSeg f,(k + 1) = LSeg (f /. (k + 1)),(f /. (k + 2))
by A2, A3, TOPREAL1:def 5;
A6:
1 < width (GoB f)
by GOBOARD7:35;
let i be Element of NAT ; ( 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * (i + 1),1 & ( ( f /. k = (GoB f) * (i + 2),1 & f /. (k + 2) = (GoB f) * (i + 1),2 ) or ( f /. (k + 2) = (GoB f) * (i + 2),1 & f /. k = (GoB f) * (i + 1),2 ) ) implies LSeg (((1 / 2) * (((GoB f) * i,1) + ((GoB f) * (i + 1),1))) - |[0 ,1]|),((1 / 2) * (((GoB f) * i,1) + ((GoB f) * (i + 1),2))) misses L~ f )
assume that
A7:
1 <= i
and
A8:
i + 2 <= len (GoB f)
and
A9:
f /. (k + 1) = (GoB f) * (i + 1),1
and
A10:
( ( f /. k = (GoB f) * (i + 2),1 & f /. (k + 2) = (GoB f) * (i + 1),2 ) or ( f /. (k + 2) = (GoB f) * (i + 2),1 & f /. k = (GoB f) * (i + 1),2 ) )
; LSeg (((1 / 2) * (((GoB f) * i,1) + ((GoB f) * (i + 1),1))) - |[0 ,1]|),((1 / 2) * (((GoB f) * i,1) + ((GoB f) * (i + 1),2))) misses L~ f
(i + 1) + 1 = i + (1 + 1)
;
then A11:
i + 1 < len (GoB f)
by A8, NAT_1:13;
then A12:
i < len (GoB f)
by NAT_1:13;
width (GoB f) <> 0
by GOBOARD1:def 5;
then A13:
0 + 1 <= width (GoB f)
by NAT_1:14;
then A14:
L~ f misses Int (cell (GoB f),i,1)
by A12, GOBOARD7:14;
0 < width (GoB f)
by A13, NAT_1:13;
then
L~ f misses Int (cell (GoB f),i,0 )
by A12, GOBOARD7:14;
then A15:
L~ f misses (Int (cell (GoB f),i,0 )) \/ (Int (cell (GoB f),i,1))
by A14, XBOOLE_1:70;
assume
LSeg (((1 / 2) * (((GoB f) * i,1) + ((GoB f) * (i + 1),1))) - |[0 ,1]|),((1 / 2) * (((GoB f) * i,1) + ((GoB f) * (i + 1),2))) meets L~ f
; contradiction
then
L~ f meets ((Int (cell (GoB f),i,0 )) \/ (Int (cell (GoB f),i,1))) \/ {((1 / 2) * (((GoB f) * i,1) + ((GoB f) * (i + 1),1)))}
by A7, A6, A12, GOBOARD6:69, XBOOLE_1:63;
then
L~ f meets {((1 / 2) * (((GoB f) * i,1) + ((GoB f) * (i + 1),1)))}
by A15, XBOOLE_1:70;
then consider k0 being Element of NAT such that
1 <= k0
and
k0 + 1 <= len f
and
A16:
LSeg (f /. (k + 1)),((GoB f) * i,1) = LSeg f,k0
by A7, A9, A13, A11, GOBOARD7:42, ZFMISC_1:56;
A17:
( LSeg f,(k + 1) c= L~ f & 1 + 1 = 2 )
by TOPREAL3:26;
( LSeg f,k0 c= L~ f & LSeg f,k c= L~ f )
by TOPREAL3:26;
hence
contradiction
by A7, A9, A10, A11, A6, A16, A17, A4, A5, GOBOARD7:63; verum