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