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