let f be non constant standard special_circular_sequence; for k being Nat st 1 <= k & k + 2 <= len f holds
for i, j being Nat st 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * (i,(j + 1)) & ( ( f /. k = (GoB f) * (i,j) & f /. (k + 2) = (GoB f) * (i,(j + 2)) ) or ( f /. (k + 2) = (GoB f) * (i,j) & f /. k = (GoB f) * (i,(j + 2)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),(j + 1))))),((1 / 2) * (((GoB f) * (i,(j + 1))) + ((GoB f) * ((i + 1),(j + 2)))))) misses L~ f
let k be Nat; ( 1 <= k & k + 2 <= len f implies for i, j being Nat st 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * (i,(j + 1)) & ( ( f /. k = (GoB f) * (i,j) & f /. (k + 2) = (GoB f) * (i,(j + 2)) ) or ( f /. (k + 2) = (GoB f) * (i,j) & f /. k = (GoB f) * (i,(j + 2)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),(j + 1))))),((1 / 2) * (((GoB f) * (i,(j + 1))) + ((GoB f) * ((i + 1),(j + 2)))))) misses L~ f )
assume that
A1:
k >= 1
and
A2:
k + 2 <= len f
; for i, j being Nat st 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * (i,(j + 1)) & ( ( f /. k = (GoB f) * (i,j) & f /. (k + 2) = (GoB f) * (i,(j + 2)) ) or ( f /. (k + 2) = (GoB f) * (i,j) & f /. k = (GoB f) * (i,(j + 2)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),(j + 1))))),((1 / 2) * (((GoB f) * (i,(j + 1))) + ((GoB f) * ((i + 1),(j + 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 + 1)) c= L~ f & LSeg (f,k) = LSeg ((f /. k),(f /. (k + 1))) )
by A1, TOPREAL1:def 3, TOPREAL3:19;
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 3;
let i, j be Nat; ( 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * (i,(j + 1)) & ( ( f /. k = (GoB f) * (i,j) & f /. (k + 2) = (GoB f) * (i,(j + 2)) ) or ( f /. (k + 2) = (GoB f) * (i,j) & f /. k = (GoB f) * (i,(j + 2)) ) ) implies LSeg (((1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),(j + 1))))),((1 / 2) * (((GoB f) * (i,(j + 1))) + ((GoB f) * ((i + 1),(j + 2)))))) misses L~ f )
assume that
A6:
1 <= i
and
A7:
i + 1 <= len (GoB f)
and
A8:
1 <= j
and
A9:
j + 2 <= width (GoB f)
and
A10:
f /. (k + 1) = (GoB f) * (i,(j + 1))
and
A11:
( ( f /. k = (GoB f) * (i,j) & f /. (k + 2) = (GoB f) * (i,(j + 2)) ) or ( f /. (k + 2) = (GoB f) * (i,j) & f /. k = (GoB f) * (i,(j + 2)) ) )
; LSeg (((1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),(j + 1))))),((1 / 2) * (((GoB f) * (i,(j + 1))) + ((GoB f) * ((i + 1),(j + 2)))))) misses L~ f
A12:
i < len (GoB f)
by A7, NAT_1:13;
j < j + 2
by XREAL_1:29;
then
j <= width (GoB f)
by A9, XXREAL_0:2;
then A13:
L~ f misses Int (cell ((GoB f),i,j))
by A12, GOBOARD7:12;
j + 1 <= j + 2
by XREAL_1:6;
then A14:
j + 1 <= width (GoB f)
by A9, XXREAL_0:2;
then
L~ f misses Int (cell ((GoB f),i,(j + 1)))
by A12, GOBOARD7:12;
then A15:
L~ f misses (Int (cell ((GoB f),i,j))) \/ (Int (cell ((GoB f),i,(j + 1))))
by A13, XBOOLE_1:70;
(j + 1) + 1 = j + (1 + 1)
;
then A16:
j + 1 < width (GoB f)
by A9, NAT_1:13;
assume
LSeg (((1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),(j + 1))))),((1 / 2) * (((GoB f) * (i,(j + 1))) + ((GoB f) * ((i + 1),(j + 2)))))) meets L~ f
; contradiction
then
L~ f meets ((Int (cell ((GoB f),i,j))) \/ (Int (cell ((GoB f),i,(j + 1))))) \/ {((1 / 2) * (((GoB f) * (i,(j + 1))) + ((GoB f) * ((i + 1),(j + 1)))))}
by A6, A8, A16, A12, GOBOARD6:64, XBOOLE_1:63;
then
( 1 <= j + 1 & L~ f meets {((1 / 2) * (((GoB f) * (i,(j + 1))) + ((GoB f) * ((i + 1),(j + 1)))))} )
by A15, NAT_1:11, XBOOLE_1:70;
then consider k0 being Nat such that
1 <= k0
and
k0 + 1 <= len f
and
A17:
LSeg ((f /. (k + 1)),((GoB f) * ((i + 1),(j + 1)))) = LSeg (f,k0)
by A6, A7, A10, A14, GOBOARD7:40, ZFMISC_1:50;
( LSeg (f,k0) c= L~ f & LSeg (f,k) c= L~ f )
by TOPREAL3:19;
hence
contradiction
by A6, A8, A10, A11, A16, A12, A17, A4, A5, GOBOARD7:59; verum