:: GOBOARD8 semantic presentation

begin


theorem :: GOBOARD8:1
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k & k + 2 <= len f holds
for i, j being Element of NAT st 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * ((i + 1),j) & f /. (k + 2) = (GoB f) * ((i + 1),(j + 2)) ) or ( f /. (k + 2) = (GoB f) * ((i + 1),j) & f /. k = (GoB f) * ((i + 1),(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
proof
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, j being Element of NAT st 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * ((i + 1),j) & f /. (k + 2) = (GoB f) * ((i + 1),(j + 2)) ) or ( f /. (k + 2) = (GoB f) * ((i + 1),j) & f /. k = (GoB f) * ((i + 1),(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 Element of NAT ; ::_thesis: ( 1 <= k & k + 2 <= len f implies for i, j being Element of NAT st 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * ((i + 1),j) & f /. (k + 2) = (GoB f) * ((i + 1),(j + 2)) ) or ( f /. (k + 2) = (GoB f) * ((i + 1),j) & f /. k = (GoB f) * ((i + 1),(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 ; ::_thesis: for i, j being Element of NAT st 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * ((i + 1),j) & f /. (k + 2) = (GoB f) * ((i + 1),(j + 2)) ) or ( f /. (k + 2) = (GoB f) * ((i + 1),j) & f /. k = (GoB f) * ((i + 1),(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 Element of NAT ; ::_thesis: ( 1 <= i & i + 1 <= len (GoB f) & 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * ((i + 1),j) & f /. (k + 2) = (GoB f) * ((i + 1),(j + 2)) ) or ( f /. (k + 2) = (GoB f) * ((i + 1),j) & f /. k = (GoB f) * ((i + 1),(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 + 1),(j + 1)) and
A11: ( ( f /. k = (GoB f) * ((i + 1),j) & f /. (k + 2) = (GoB f) * ((i + 1),(j + 2)) ) or ( f /. (k + 2) = (GoB f) * ((i + 1),j) & f /. k = (GoB f) * ((i + 1),(j + 2)) ) ) ; ::_thesis: 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 ; ::_thesis: 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 Element of NAT  such that
 1 <= k0 and
 k0 + 1 <= len f and
A17: LSeg ((f /. (k + 1)),((GoB f) * (i,(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:60; ::_thesis: verum
end;

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

theorem :: GOBOARD8:3
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k & k + 2 <= len f holds
for i, j being Element of NAT st 1 <= i & i + 2 <= len (GoB f) & 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * ((i + 2),(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 1),j) ) or ( f /. (k + 2) = (GoB f) * ((i + 2),(j + 1)) & f /. k = (GoB f) * ((i + 1),j) ) ) 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
proof
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, j being Element of NAT st 1 <= i & i + 2 <= len (GoB f) & 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * ((i + 2),(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 1),j) ) or ( f /. (k + 2) = (GoB f) * ((i + 2),(j + 1)) & f /. k = (GoB f) * ((i + 1),j) ) ) 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 Element of NAT ; ::_thesis: ( 1 <= k & k + 2 <= len f implies for i, j being Element of NAT st 1 <= i & i + 2 <= len (GoB f) & 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * ((i + 2),(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 1),j) ) or ( f /. (k + 2) = (GoB f) * ((i + 2),(j + 1)) & f /. k = (GoB f) * ((i + 1),j) ) ) 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 ; ::_thesis: for i, j being Element of NAT st 1 <= i & i + 2 <= len (GoB f) & 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * ((i + 2),(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 1),j) ) or ( f /. (k + 2) = (GoB f) * ((i + 2),(j + 1)) & f /. k = (GoB f) * ((i + 1),j) ) ) 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 Element of NAT ; ::_thesis: ( 1 <= i & i + 2 <= len (GoB f) & 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * ((i + 2),(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 1),j) ) or ( f /. (k + 2) = (GoB f) * ((i + 2),(j + 1)) & f /. k = (GoB f) * ((i + 1),j) ) ) 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 + 2 <= len (GoB f) and
A8: 1 <= j and
A9: j + 2 <= width (GoB f) and
A10: f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) and
A11: ( ( f /. k = (GoB f) * ((i + 2),(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 1),j) ) or ( f /. (k + 2) = (GoB f) * ((i + 2),(j + 1)) & f /. k = (GoB f) * ((i + 1),j) ) ) ; ::_thesis: 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
 (i + 1) + 1 = i + (1 + 1) ;
then A12: i + 1 < len (GoB f) by A7, NAT_1:13;
then A13: i < len (GoB f) by NAT_1:13;
 j + 1 <= j + 2 by XREAL_1:6;
then A14: j + 1 <= width (GoB f) by A9, XXREAL_0:2;
then A15: L~ f misses Int (cell ((GoB f),i,(j + 1))) by A13, GOBOARD7:12;
 (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 ; ::_thesis: contradiction
then A17: 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, A13, GOBOARD6:64, XBOOLE_1:63;
 j < j + 2 by XREAL_1:29;
then A18: j < width (GoB f) by A9, XXREAL_0:2;
then  L~ f misses Int (cell ((GoB f),i,j)) by A13, GOBOARD7:12;
then  L~ f misses (Int (cell ((GoB f),i,j))) \/ (Int (cell ((GoB f),i,(j + 1)))) by A15, XBOOLE_1:70;
then  ( 1 <= j + 1 & L~ f meets {((1 / 2) * (((GoB f) * (i,(j + 1))) + ((GoB f) * ((i + 1),(j + 1)))))} ) by A17, NAT_1:11, XBOOLE_1:70;
then consider k0 being Element of NAT  such that
 1 <= k0 and
 k0 + 1 <= len f and
A19: LSeg ((f /. (k + 1)),((GoB f) * (i,(j + 1)))) = LSeg (f,k0) by A6, A10, A14, A12, 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, A18, A12, A19, A4, A5, GOBOARD7:62; ::_thesis: verum
end;

theorem :: GOBOARD8:4
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k & k + 2 <= len f holds
for i, j being Element of 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
proof
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, j being Element of 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 Element of NAT ; ::_thesis: ( 1 <= k & k + 2 <= len f implies for i, j being Element of 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 ; ::_thesis: for i, j being Element of 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 Element of NAT ; ::_thesis: ( 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)) ) ) ; ::_thesis: 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 ; ::_thesis: 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 Element of 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; ::_thesis: verum
end;

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

theorem :: GOBOARD8:6
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k & k + 2 <= len f holds
for i, j being Element of NAT st 1 <= i & i + 2 <= len (GoB f) & 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * (i,(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 1),j) ) or ( f /. (k + 2) = (GoB f) * (i,(j + 1)) & f /. k = (GoB f) * ((i + 1),j) ) ) holds
LSeg (((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 2),(j + 1))))),((1 / 2) * (((GoB f) * ((i + 1),(j + 1))) + ((GoB f) * ((i + 2),(j + 2)))))) misses L~ f
proof
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, j being Element of NAT st 1 <= i & i + 2 <= len (GoB f) & 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * (i,(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 1),j) ) or ( f /. (k + 2) = (GoB f) * (i,(j + 1)) & f /. k = (GoB f) * ((i + 1),j) ) ) holds
LSeg (((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 2),(j + 1))))),((1 / 2) * (((GoB f) * ((i + 1),(j + 1))) + ((GoB f) * ((i + 2),(j + 2)))))) misses L~ f
let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 2 <= len f implies for i, j being Element of NAT st 1 <= i & i + 2 <= len (GoB f) & 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * (i,(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 1),j) ) or ( f /. (k + 2) = (GoB f) * (i,(j + 1)) & f /. k = (GoB f) * ((i + 1),j) ) ) holds
LSeg (((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 2),(j + 1))))),((1 / 2) * (((GoB f) * ((i + 1),(j + 1))) + ((GoB f) * ((i + 2),(j + 2)))))) misses L~ f )
assume that
A1: k >= 1 and
A2: k + 2 <= len f ; ::_thesis: for i, j being Element of NAT st 1 <= i & i + 2 <= len (GoB f) & 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * (i,(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 1),j) ) or ( f /. (k + 2) = (GoB f) * (i,(j + 1)) & f /. k = (GoB f) * ((i + 1),j) ) ) holds
LSeg (((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 2),(j + 1))))),((1 / 2) * (((GoB f) * ((i + 1),(j + 1))) + ((GoB f) * ((i + 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 + 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 Element of NAT ; ::_thesis: ( 1 <= i & i + 2 <= len (GoB f) & 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * (i,(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 1),j) ) or ( f /. (k + 2) = (GoB f) * (i,(j + 1)) & f /. k = (GoB f) * ((i + 1),j) ) ) implies LSeg (((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 2),(j + 1))))),((1 / 2) * (((GoB f) * ((i + 1),(j + 1))) + ((GoB f) * ((i + 2),(j + 2)))))) misses L~ f )
assume that
A6: 1 <= i and
A7: i + 2 <= len (GoB f) and
A8: 1 <= j and
A9: j + 2 <= width (GoB f) and
A10: f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) and
A11: ( ( f /. k = (GoB f) * (i,(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 1),j) ) or ( f /. (k + 2) = (GoB f) * (i,(j + 1)) & f /. k = (GoB f) * ((i + 1),j) ) ) ; ::_thesis: LSeg (((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 2),(j + 1))))),((1 / 2) * (((GoB f) * ((i + 1),(j + 1))) + ((GoB f) * ((i + 2),(j + 2)))))) misses L~ f
A12: (i + 1) + 1 = i + (1 + 1) ;
then A13: i + 1 < len (GoB f) by A7, NAT_1:13;
 j + 1 <= j + 2 by XREAL_1:6;
then A14: j + 1 <= width (GoB f) by A9, XXREAL_0:2;
then A15: L~ f misses Int (cell ((GoB f),(i + 1),(j + 1))) by A13, GOBOARD7:12;
 (j + 1) + 1 = j + (1 + 1) ;
then A16: j + 1 < width (GoB f) by A9, NAT_1:13;
A17: 1 <= i + 1 by NAT_1:11;
 j < j + 2 by XREAL_1:29;
then A18: j < width (GoB f) by A9, XXREAL_0:2;
then  L~ f misses Int (cell ((GoB f),(i + 1),j)) by A13, GOBOARD7:12;
then A19: L~ f misses (Int (cell ((GoB f),(i + 1),j))) \/ (Int (cell ((GoB f),(i + 1),(j + 1)))) by A15, XBOOLE_1:70;
assume  LSeg (((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 2),(j + 1))))),((1 / 2) * (((GoB f) * ((i + 1),(j + 1))) + ((GoB f) * ((i + 2),(j + 2)))))) meets L~ f ; ::_thesis: contradiction
then  L~ f meets ((Int (cell ((GoB f),(i + 1),j))) \/ (Int (cell ((GoB f),(i + 1),(j + 1))))) \/ {((1 / 2) * (((GoB f) * ((i + 1),(j + 1))) + ((GoB f) * ((i + 2),(j + 1)))))} by A8, A12, A13, A16, A17, GOBOARD6:64, XBOOLE_1:63;
then  ( 1 <= j + 1 & L~ f meets {((1 / 2) * (((GoB f) * ((i + 1),(j + 1))) + ((GoB f) * ((i + 2),(j + 1)))))} ) by A19, NAT_1:11, XBOOLE_1:70;
then consider k0 being Element of NAT  such that
 1 <= k0 and
 k0 + 1 <= len f and
A20: LSeg ((f /. (k + 1)),((GoB f) * ((i + 2),(j + 1)))) = LSeg (f,k0) by A7, A10, A14, A12, A17, 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, A18, A13, A20, A4, A5, GOBOARD7:62; ::_thesis: verum
end;

theorem :: GOBOARD8:7
for f being 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
proof
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),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 ; ::_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),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 ; ::_thesis: 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_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 < width (GoB f) by GOBOARD7:33;
let i be Element of NAT ; ::_thesis: ( 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) ) ) ; ::_thesis: 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_3;
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:12;
 0 < width (GoB f) by A13, NAT_1:13;
then  L~ f misses Int (cell ((GoB f),i,0)) by A12, GOBOARD7:12;
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 ; ::_thesis: 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:66, 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:40, ZFMISC_1:50;
A17: ( 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, A11, A6, A16, A17, A4, A5, GOBOARD7:61; ::_thesis: verum
end;

theorem :: GOBOARD8:8
for f being 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,1) & f /. (k + 2) = (GoB f) * ((i + 1),2) ) or ( f /. (k + 2) = (GoB f) * (i,1) & f /. k = (GoB f) * ((i + 1),2) ) ) holds
LSeg ((((1 / 2) * (((GoB f) * ((i + 1),1)) + ((GoB f) * ((i + 2),1)))) - |[0,1]|),((1 / 2) * (((GoB f) * ((i + 1),1)) + ((GoB f) * ((i + 2),2))))) misses L~ f
proof
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),1) & ( ( f /. k = (GoB f) * (i,1) & f /. (k + 2) = (GoB f) * ((i + 1),2) ) or ( f /. (k + 2) = (GoB f) * (i,1) & f /. k = (GoB f) * ((i + 1),2) ) ) holds
LSeg ((((1 / 2) * (((GoB f) * ((i + 1),1)) + ((GoB f) * ((i + 2),1)))) - |[0,1]|),((1 / 2) * (((GoB f) * ((i + 1),1)) + ((GoB f) * ((i + 2),2))))) 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),1) & ( ( f /. k = (GoB f) * (i,1) & f /. (k + 2) = (GoB f) * ((i + 1),2) ) or ( f /. (k + 2) = (GoB f) * (i,1) & f /. k = (GoB f) * ((i + 1),2) ) ) holds
LSeg ((((1 / 2) * (((GoB f) * ((i + 1),1)) + ((GoB f) * ((i + 2),1)))) - |[0,1]|),((1 / 2) * (((GoB f) * ((i + 1),1)) + ((GoB f) * ((i + 2),2))))) 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),1) & ( ( f /. k = (GoB f) * (i,1) & f /. (k + 2) = (GoB f) * ((i + 1),2) ) or ( f /. (k + 2) = (GoB f) * (i,1) & f /. k = (GoB f) * ((i + 1),2) ) ) holds
LSeg ((((1 / 2) * (((GoB f) * ((i + 1),1)) + ((GoB f) * ((i + 2),1)))) - |[0,1]|),((1 / 2) * (((GoB f) * ((i + 1),1)) + ((GoB f) * ((i + 2),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 < width (GoB f) by GOBOARD7:33;
let i be Element of NAT ; ::_thesis: ( 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),1) & ( ( f /. k = (GoB f) * (i,1) & f /. (k + 2) = (GoB f) * ((i + 1),2) ) or ( f /. (k + 2) = (GoB f) * (i,1) & f /. k = (GoB f) * ((i + 1),2) ) ) implies LSeg ((((1 / 2) * (((GoB f) * ((i + 1),1)) + ((GoB f) * ((i + 2),1)))) - |[0,1]|),((1 / 2) * (((GoB f) * ((i + 1),1)) + ((GoB f) * ((i + 2),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,1) & f /. (k + 2) = (GoB f) * ((i + 1),2) ) or ( f /. (k + 2) = (GoB f) * (i,1) & f /. k = (GoB f) * ((i + 1),2) ) ) ; ::_thesis: LSeg ((((1 / 2) * (((GoB f) * ((i + 1),1)) + ((GoB f) * ((i + 2),1)))) - |[0,1]|),((1 / 2) * (((GoB f) * ((i + 1),1)) + ((GoB f) * ((i + 2),2))))) misses L~ f
A11: (i + 1) + 1 = i + (1 + 1) ;
then A12: i + 1 < len (GoB f) by A8, NAT_1:13;
 width (GoB f) <> 0 by GOBOARD1:def_3;
then A13: 0 + 1 <= width (GoB f) by NAT_1:14;
then A14: L~ f misses Int (cell ((GoB f),(i + 1),1)) by A12, GOBOARD7:12;
 0 < width (GoB f) by A13, NAT_1:13;
then  L~ f misses Int (cell ((GoB f),(i + 1),0)) by A12, GOBOARD7:12;
then A15: L~ f misses (Int (cell ((GoB f),(i + 1),0))) \/ (Int (cell ((GoB f),(i + 1),1))) by A14, XBOOLE_1:70;
A16: 1 <= i + 1 by NAT_1:11;
assume  LSeg ((((1 / 2) * (((GoB f) * ((i + 1),1)) + ((GoB f) * ((i + 2),1)))) - |[0,1]|),((1 / 2) * (((GoB f) * ((i + 1),1)) + ((GoB f) * ((i + 2),2))))) meets L~ f ; ::_thesis: contradiction
then  L~ f meets ((Int (cell ((GoB f),(i + 1),0))) \/ (Int (cell ((GoB f),(i + 1),1)))) \/ {((1 / 2) * (((GoB f) * ((i + 1),1)) + ((GoB f) * ((i + 2),1))))} by A11, A12, A6, A16, GOBOARD6:66, XBOOLE_1:63;
then  L~ f meets {((1 / 2) * (((GoB f) * ((i + 1),1)) + ((GoB f) * ((i + 2),1))))} by A15, XBOOLE_1:70;
then consider k0 being Element of NAT  such that
 1 <= k0 and
 k0 + 1 <= len f and
A17: LSeg ((f /. (k + 1)),((GoB f) * ((i + 2),1))) = LSeg (f,k0) by A8, A9, A13, A11, A16, GOBOARD7:40, 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:61; ::_thesis: verum
end;

theorem :: GOBOARD8:9
for f being 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),(width (GoB f))) & ( ( f /. k = (GoB f) * ((i + 2),(width (GoB f))) & f /. (k + 2) = (GoB f) * ((i + 1),((width (GoB f)) -' 1)) ) or ( f /. (k + 2) = (GoB f) * ((i + 2),(width (GoB f))) & f /. k = (GoB f) * ((i + 1),((width (GoB f)) -' 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|)) misses L~ f
proof
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 + 2),(width (GoB f))) & f /. (k + 2) = (GoB f) * ((i + 1),((width (GoB f)) -' 1)) ) or ( f /. (k + 2) = (GoB f) * ((i + 2),(width (GoB f))) & f /. k = (GoB f) * ((i + 1),((width (GoB f)) -' 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(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 + 2),(width (GoB f))) & f /. (k + 2) = (GoB f) * ((i + 1),((width (GoB f)) -' 1)) ) or ( f /. (k + 2) = (GoB f) * ((i + 2),(width (GoB f))) & f /. k = (GoB f) * ((i + 1),((width (GoB f)) -' 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(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 + 2),(width (GoB f))) & f /. (k + 2) = (GoB f) * ((i + 1),((width (GoB f)) -' 1)) ) or ( f /. (k + 2) = (GoB f) * ((i + 2),(width (GoB f))) & f /. k = (GoB f) * ((i + 1),((width (GoB f)) -' 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(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_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 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 + 2),(width (GoB f))) & f /. (k + 2) = (GoB f) * ((i + 1),((width (GoB f)) -' 1)) ) or ( f /. (k + 2) = (GoB f) * ((i + 2),(width (GoB f))) & f /. k = (GoB f) * ((i + 1),((width (GoB f)) -' 1)) ) ) implies LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(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 + 2),(width (GoB f))) & f /. (k + 2) = (GoB f) * ((i + 1),((width (GoB f)) -' 1)) ) or ( f /. (k + 2) = (GoB f) * ((i + 2),(width (GoB f))) & f /. k = (GoB f) * ((i + 1),((width (GoB f)) -' 1)) ) ) ; ::_thesis: LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|)) misses L~ f
 (i + 1) + 1 = i + (1 + 1) ;
then A10: i + 1 < len (GoB f) by A7, NAT_1:13;
then A11: i < len (GoB f) by NAT_1:13;
then A12: L~ f misses Int (cell ((GoB f),i,(width (GoB f)))) by GOBOARD7:12;
assume A13: LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|)) meets L~ f ; ::_thesis: contradiction
A14: 1 < width (GoB f) by GOBOARD7:33;
then A15: ((width (GoB f)) -' 1) + 1 = width (GoB f) by XREAL_1:235;
then A16: (width (GoB f)) -' 1 < width (GoB f) by NAT_1:13;
then  L~ f misses Int (cell ((GoB f),i,((width (GoB f)) -' 1))) by A11, GOBOARD7:12;
then A17: L~ f misses (Int (cell ((GoB f),i,((width (GoB f)) -' 1)))) \/ (Int (cell ((GoB f),i,(width (GoB f))))) by A12, XBOOLE_1:70;
A18: 1 <= (width (GoB f)) -' 1 by A14, A15, NAT_1:13;
then  (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) = (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),((width (GoB f)) -' 1)))) by A6, A15, A10, GOBOARD7:9;
then  L~ f meets ((Int (cell ((GoB f),i,((width (GoB f)) -' 1)))) \/ (Int (cell ((GoB f),i,(width (GoB f)))))) \/ {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} by A6, A14, A11, A13, GOBOARD6:67, XBOOLE_1:63;
then  L~ f meets {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} by A17, XBOOLE_1:70;
then consider k0 being Element of NAT  such that
 1 <= k0 and
 k0 + 1 <= len f and
A19: LSeg ((f /. (k + 1)),((GoB f) * (i,(width (GoB f))))) = LSeg (f,k0) by A6, A8, A14, A10, 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, A9, A15, A18, A16, A10, A19, A4, A5, GOBOARD7:62; ::_thesis: verum
end;

theorem :: GOBOARD8:10
for f being 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),(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
proof
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_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 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:12;
A13: 1 <= width (GoB f) by GOBOARD7:33;
then A14: ((width (GoB f)) -' 1) + 1 = width (GoB f) by XREAL_1:235;
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:12;
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:33;
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:9;
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:67, 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:40, ZFMISC_1:50;
 ( LSeg (f,k0) c= L~ f & LSeg (f,k) c= L~ f ) by TOPREAL3:19;
hence  contradiction by A6, A8, A9, A14, A20, A15, A11, A21, A4, A5, GOBOARD7:62; ::_thesis: verum
end;

theorem :: GOBOARD8:11
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k & k + 2 <= len f holds
for i, j being Element of NAT st 1 <= j & j + 1 <= width (GoB f) & 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * (i,(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 2),(j + 1)) ) or ( f /. (k + 2) = (GoB f) * (i,(j + 1)) & f /. k = (GoB f) * ((i + 2),(j + 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),(j + 1))))),((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 2),(j + 1)))))) misses L~ f
proof
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, j being Element of NAT st 1 <= j & j + 1 <= width (GoB f) & 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * (i,(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 2),(j + 1)) ) or ( f /. (k + 2) = (GoB f) * (i,(j + 1)) & f /. k = (GoB f) * ((i + 2),(j + 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),(j + 1))))),((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 2),(j + 1)))))) misses L~ f
let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 2 <= len f implies for i, j being Element of NAT st 1 <= j & j + 1 <= width (GoB f) & 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * (i,(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 2),(j + 1)) ) or ( f /. (k + 2) = (GoB f) * (i,(j + 1)) & f /. k = (GoB f) * ((i + 2),(j + 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),(j + 1))))),((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 2),(j + 1)))))) misses L~ f )
assume that
A1: k >= 1 and
A2: k + 2 <= len f ; ::_thesis: for i, j being Element of NAT st 1 <= j & j + 1 <= width (GoB f) & 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * (i,(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 2),(j + 1)) ) or ( f /. (k + 2) = (GoB f) * (i,(j + 1)) & f /. k = (GoB f) * ((i + 2),(j + 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),(j + 1))))),((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 2),(j + 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_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 Element of NAT ; ::_thesis: ( 1 <= j & j + 1 <= width (GoB f) & 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * (i,(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 2),(j + 1)) ) or ( f /. (k + 2) = (GoB f) * (i,(j + 1)) & f /. k = (GoB f) * ((i + 2),(j + 1)) ) ) implies LSeg (((1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),(j + 1))))),((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 2),(j + 1)))))) misses L~ f )
assume that
A6: 1 <= j and
A7: j + 1 <= width (GoB f) and
A8: 1 <= i and
A9: i + 2 <= len (GoB f) and
A10: f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) and
A11: ( ( f /. k = (GoB f) * (i,(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 2),(j + 1)) ) or ( f /. (k + 2) = (GoB f) * (i,(j + 1)) & f /. k = (GoB f) * ((i + 2),(j + 1)) ) ) ; ::_thesis: LSeg (((1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),(j + 1))))),((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 2),(j + 1)))))) misses L~ f
A12: j < width (GoB f) by A7, NAT_1:13;
 i < i + 2 by XREAL_1:29;
then  i <= len (GoB f) by A9, XXREAL_0:2;
then A13: L~ f misses Int (cell ((GoB f),i,j)) by A12, GOBOARD7:12;
 i + 1 <= i + 2 by XREAL_1:6;
then A14: i + 1 <= len (GoB f) by A9, XXREAL_0:2;
then  L~ f misses Int (cell ((GoB f),(i + 1),j)) by A12, GOBOARD7:12;
then A15: L~ f misses (Int (cell ((GoB f),i,j))) \/ (Int (cell ((GoB f),(i + 1),j))) by A13, XBOOLE_1:70;
 (i + 1) + 1 = i + (1 + 1) ;
then A16: i + 1 < len (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 + 1),j)) + ((GoB f) * ((i + 2),(j + 1)))))) meets L~ f ; ::_thesis: contradiction
then  L~ f meets ((Int (cell ((GoB f),i,j))) \/ (Int (cell ((GoB f),(i + 1),j)))) \/ {((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 1),(j + 1)))))} by A6, A8, A16, A12, GOBOARD6:65, XBOOLE_1:63;
then  ( 1 <= i + 1 & L~ f meets {((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 1),(j + 1)))))} ) by A15, NAT_1:11, XBOOLE_1:70;
then consider k0 being Element of NAT  such that
 1 <= k0 and
 k0 + 1 <= len f and
A17: LSeg ((f /. (k + 1)),((GoB f) * ((i + 1),j))) = LSeg (f,k0) by A6, A7, A10, A14, GOBOARD7:39, 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:62; ::_thesis: verum
end;

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

theorem :: GOBOARD8:13
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k & k + 2 <= len f holds
for j, i being Element of NAT st 1 <= j & j + 2 <= width (GoB f) & 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * ((i + 1),(j + 2)) & f /. (k + 2) = (GoB f) * (i,(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((i + 1),(j + 2)) & f /. k = (GoB f) * (i,(j + 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),(j + 1))))),((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 2),(j + 1)))))) misses L~ f
proof
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 j, i being Element of NAT st 1 <= j & j + 2 <= width (GoB f) & 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * ((i + 1),(j + 2)) & f /. (k + 2) = (GoB f) * (i,(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((i + 1),(j + 2)) & f /. k = (GoB f) * (i,(j + 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),(j + 1))))),((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 2),(j + 1)))))) misses L~ f
let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 2 <= len f implies for j, i being Element of NAT st 1 <= j & j + 2 <= width (GoB f) & 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * ((i + 1),(j + 2)) & f /. (k + 2) = (GoB f) * (i,(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((i + 1),(j + 2)) & f /. k = (GoB f) * (i,(j + 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),(j + 1))))),((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 2),(j + 1)))))) misses L~ f )
assume that
A1: k >= 1 and
A2: k + 2 <= len f ; ::_thesis: for j, i being Element of NAT st 1 <= j & j + 2 <= width (GoB f) & 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * ((i + 1),(j + 2)) & f /. (k + 2) = (GoB f) * (i,(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((i + 1),(j + 2)) & f /. k = (GoB f) * (i,(j + 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),(j + 1))))),((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 2),(j + 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_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 j, i be Element of NAT ; ::_thesis: ( 1 <= j & j + 2 <= width (GoB f) & 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * ((i + 1),(j + 2)) & f /. (k + 2) = (GoB f) * (i,(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((i + 1),(j + 2)) & f /. k = (GoB f) * (i,(j + 1)) ) ) implies LSeg (((1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),(j + 1))))),((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 2),(j + 1)))))) misses L~ f )
assume that
A6: 1 <= j and
A7: j + 2 <= width (GoB f) and
A8: 1 <= i and
A9: i + 2 <= len (GoB f) and
A10: f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) and
A11: ( ( f /. k = (GoB f) * ((i + 1),(j + 2)) & f /. (k + 2) = (GoB f) * (i,(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((i + 1),(j + 2)) & f /. k = (GoB f) * (i,(j + 1)) ) ) ; ::_thesis: LSeg (((1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),(j + 1))))),((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 2),(j + 1)))))) misses L~ f
 (j + 1) + 1 = j + (1 + 1) ;
then A12: j + 1 < width (GoB f) by A7, NAT_1:13;
then A13: j < width (GoB f) by NAT_1:13;
 i + 1 <= i + 2 by XREAL_1:6;
then A14: i + 1 <= len (GoB f) by A9, XXREAL_0:2;
then A15: L~ f misses Int (cell ((GoB f),(i + 1),j)) by A13, GOBOARD7:12;
 (i + 1) + 1 = i + (1 + 1) ;
then A16: i + 1 < len (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 + 1),j)) + ((GoB f) * ((i + 2),(j + 1)))))) meets L~ f ; ::_thesis: contradiction
then A17: L~ f meets ((Int (cell ((GoB f),i,j))) \/ (Int (cell ((GoB f),(i + 1),j)))) \/ {((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 1),(j + 1)))))} by A6, A8, A16, A13, GOBOARD6:65, XBOOLE_1:63;
 i < i + 2 by XREAL_1:29;
then A18: i < len (GoB f) by A9, XXREAL_0:2;
then  L~ f misses Int (cell ((GoB f),i,j)) by A13, GOBOARD7:12;
then  L~ f misses (Int (cell ((GoB f),i,j))) \/ (Int (cell ((GoB f),(i + 1),j))) by A15, XBOOLE_1:70;
then  ( 1 <= i + 1 & L~ f meets {((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 1),(j + 1)))))} ) by A17, NAT_1:11, XBOOLE_1:70;
then consider k0 being Element of NAT  such that
 1 <= k0 and
 k0 + 1 <= len f and
A19: LSeg ((f /. (k + 1)),((GoB f) * ((i + 1),j))) = LSeg (f,k0) by A6, A10, A14, A12, GOBOARD7:39, 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, A18, A12, A19, A4, A5, GOBOARD7:60; ::_thesis: verum
end;

theorem :: GOBOARD8:14
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k & k + 2 <= len f holds
for j, i being Element of NAT st 1 <= j & j + 1 <= width (GoB f) & 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),j) & ( ( f /. k = (GoB f) * (i,j) & f /. (k + 2) = (GoB f) * ((i + 2),j) ) or ( f /. (k + 2) = (GoB f) * (i,j) & f /. k = (GoB f) * ((i + 2),j) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),(j + 1))))),((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 2),(j + 1)))))) misses L~ f
proof
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 j, i being Element of NAT st 1 <= j & j + 1 <= width (GoB f) & 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),j) & ( ( f /. k = (GoB f) * (i,j) & f /. (k + 2) = (GoB f) * ((i + 2),j) ) or ( f /. (k + 2) = (GoB f) * (i,j) & f /. k = (GoB f) * ((i + 2),j) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),(j + 1))))),((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 2),(j + 1)))))) misses L~ f
let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 2 <= len f implies for j, i being Element of NAT st 1 <= j & j + 1 <= width (GoB f) & 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),j) & ( ( f /. k = (GoB f) * (i,j) & f /. (k + 2) = (GoB f) * ((i + 2),j) ) or ( f /. (k + 2) = (GoB f) * (i,j) & f /. k = (GoB f) * ((i + 2),j) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),(j + 1))))),((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 2),(j + 1)))))) misses L~ f )
assume that
A1: k >= 1 and
A2: k + 2 <= len f ; ::_thesis: for j, i being Element of NAT st 1 <= j & j + 1 <= width (GoB f) & 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),j) & ( ( f /. k = (GoB f) * (i,j) & f /. (k + 2) = (GoB f) * ((i + 2),j) ) or ( f /. (k + 2) = (GoB f) * (i,j) & f /. k = (GoB f) * ((i + 2),j) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),(j + 1))))),((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 2),(j + 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_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 j, i be Element of NAT ; ::_thesis: ( 1 <= j & j + 1 <= width (GoB f) & 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),j) & ( ( f /. k = (GoB f) * (i,j) & f /. (k + 2) = (GoB f) * ((i + 2),j) ) or ( f /. (k + 2) = (GoB f) * (i,j) & f /. k = (GoB f) * ((i + 2),j) ) ) implies LSeg (((1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),(j + 1))))),((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 2),(j + 1)))))) misses L~ f )
assume that
A6: 1 <= j and
A7: j + 1 <= width (GoB f) and
A8: 1 <= i and
A9: i + 2 <= len (GoB f) and
A10: f /. (k + 1) = (GoB f) * ((i + 1),j) and
A11: ( ( f /. k = (GoB f) * (i,j) & f /. (k + 2) = (GoB f) * ((i + 2),j) ) or ( f /. (k + 2) = (GoB f) * (i,j) & f /. k = (GoB f) * ((i + 2),j) ) ) ; ::_thesis: LSeg (((1 / 2) * (((GoB f) * (i,j)) + ((GoB f) * ((i + 1),(j + 1))))),((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 2),(j + 1)))))) misses L~ f
A12: j < width (GoB f) by A7, NAT_1:13;
 i < i + 2 by XREAL_1:29;
then  i <= len (GoB f) by A9, XXREAL_0:2;
then A13: L~ f misses Int (cell ((GoB f),i,j)) by A12, GOBOARD7:12;
 i + 1 <= i + 2 by XREAL_1:6;
then A14: i + 1 <= len (GoB f) by A9, XXREAL_0:2;
then  L~ f misses Int (cell ((GoB f),(i + 1),j)) by A12, GOBOARD7:12;
then A15: L~ f misses (Int (cell ((GoB f),i,j))) \/ (Int (cell ((GoB f),(i + 1),j))) by A13, XBOOLE_1:70;
 (i + 1) + 1 = i + (1 + 1) ;
then A16: i + 1 < len (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 + 1),j)) + ((GoB f) * ((i + 2),(j + 1)))))) meets L~ f ; ::_thesis: contradiction
then  L~ f meets ((Int (cell ((GoB f),i,j))) \/ (Int (cell ((GoB f),(i + 1),j)))) \/ {((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 1),(j + 1)))))} by A6, A8, A16, A12, GOBOARD6:65, XBOOLE_1:63;
then  ( 1 <= i + 1 & L~ f meets {((1 / 2) * (((GoB f) * ((i + 1),j)) + ((GoB f) * ((i + 1),(j + 1)))))} ) by A15, NAT_1:11, XBOOLE_1:70;
then consider k0 being Element of 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:39, 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:61; ::_thesis: verum
end;

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

theorem :: GOBOARD8:16
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k & k + 2 <= len f holds
for j, i being Element of NAT st 1 <= j & j + 2 <= width (GoB f) & 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * ((i + 1),j) & f /. (k + 2) = (GoB f) * (i,(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((i + 1),j) & f /. k = (GoB f) * (i,(j + 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,(j + 1))) + ((GoB f) * ((i + 1),(j + 2))))),((1 / 2) * (((GoB f) * ((i + 1),(j + 1))) + ((GoB f) * ((i + 2),(j + 2)))))) misses L~ f
proof
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 j, i being Element of NAT st 1 <= j & j + 2 <= width (GoB f) & 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * ((i + 1),j) & f /. (k + 2) = (GoB f) * (i,(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((i + 1),j) & f /. k = (GoB f) * (i,(j + 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,(j + 1))) + ((GoB f) * ((i + 1),(j + 2))))),((1 / 2) * (((GoB f) * ((i + 1),(j + 1))) + ((GoB f) * ((i + 2),(j + 2)))))) misses L~ f
let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 2 <= len f implies for j, i being Element of NAT st 1 <= j & j + 2 <= width (GoB f) & 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * ((i + 1),j) & f /. (k + 2) = (GoB f) * (i,(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((i + 1),j) & f /. k = (GoB f) * (i,(j + 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,(j + 1))) + ((GoB f) * ((i + 1),(j + 2))))),((1 / 2) * (((GoB f) * ((i + 1),(j + 1))) + ((GoB f) * ((i + 2),(j + 2)))))) misses L~ f )
assume that
A1: k >= 1 and
A2: k + 2 <= len f ; ::_thesis: for j, i being Element of NAT st 1 <= j & j + 2 <= width (GoB f) & 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * ((i + 1),j) & f /. (k + 2) = (GoB f) * (i,(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((i + 1),j) & f /. k = (GoB f) * (i,(j + 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,(j + 1))) + ((GoB f) * ((i + 1),(j + 2))))),((1 / 2) * (((GoB f) * ((i + 1),(j + 1))) + ((GoB f) * ((i + 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 + 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 j, i be Element of NAT ; ::_thesis: ( 1 <= j & j + 2 <= width (GoB f) & 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * ((i + 1),j) & f /. (k + 2) = (GoB f) * (i,(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((i + 1),j) & f /. k = (GoB f) * (i,(j + 1)) ) ) implies LSeg (((1 / 2) * (((GoB f) * (i,(j + 1))) + ((GoB f) * ((i + 1),(j + 2))))),((1 / 2) * (((GoB f) * ((i + 1),(j + 1))) + ((GoB f) * ((i + 2),(j + 2)))))) misses L~ f )
assume that
A6: 1 <= j and
A7: j + 2 <= width (GoB f) and
A8: 1 <= i and
A9: i + 2 <= len (GoB f) and
A10: f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) and
A11: ( ( f /. k = (GoB f) * ((i + 1),j) & f /. (k + 2) = (GoB f) * (i,(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((i + 1),j) & f /. k = (GoB f) * (i,(j + 1)) ) ) ; ::_thesis: LSeg (((1 / 2) * (((GoB f) * (i,(j + 1))) + ((GoB f) * ((i + 1),(j + 2))))),((1 / 2) * (((GoB f) * ((i + 1),(j + 1))) + ((GoB f) * ((i + 2),(j + 2)))))) misses L~ f
A12: (j + 1) + 1 = j + (1 + 1) ;
then A13: j + 1 < width (GoB f) by A7, NAT_1:13;
 i + 1 <= i + 2 by XREAL_1:6;
then A14: i + 1 <= len (GoB f) by A9, XXREAL_0:2;
then A15: L~ f misses Int (cell ((GoB f),(i + 1),(j + 1))) by A13, GOBOARD7:12;
 (i + 1) + 1 = i + (1 + 1) ;
then A16: i + 1 < len (GoB f) by A9, NAT_1:13;
A17: 1 <= j + 1 by NAT_1:11;
 i < i + 2 by XREAL_1:29;
then A18: i < len (GoB f) by A9, XXREAL_0:2;
then  L~ f misses Int (cell ((GoB f),i,(j + 1))) by A13, GOBOARD7:12;
then A19: L~ f misses (Int (cell ((GoB f),i,(j + 1)))) \/ (Int (cell ((GoB f),(i + 1),(j + 1)))) by A15, XBOOLE_1:70;
assume  LSeg (((1 / 2) * (((GoB f) * (i,(j + 1))) + ((GoB f) * ((i + 1),(j + 2))))),((1 / 2) * (((GoB f) * ((i + 1),(j + 1))) + ((GoB f) * ((i + 2),(j + 2)))))) meets L~ f ; ::_thesis: contradiction
then  L~ f meets ((Int (cell ((GoB f),i,(j + 1)))) \/ (Int (cell ((GoB f),(i + 1),(j + 1))))) \/ {((1 / 2) * (((GoB f) * ((i + 1),(j + 1))) + ((GoB f) * ((i + 1),(j + 2)))))} by A8, A12, A13, A16, A17, GOBOARD6:65, XBOOLE_1:63;
then  ( 1 <= i + 1 & L~ f meets {((1 / 2) * (((GoB f) * ((i + 1),(j + 1))) + ((GoB f) * ((i + 1),(j + 2)))))} ) by A19, NAT_1:11, XBOOLE_1:70;
then consider k0 being Element of NAT  such that
 1 <= k0 and
 k0 + 1 <= len f and
A20: LSeg ((f /. (k + 1)),((GoB f) * ((i + 1),(j + 2)))) = LSeg (f,k0) by A7, A10, A14, A12, A17, GOBOARD7:39, 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, A18, A13, A20, A4, A5, GOBOARD7:60; ::_thesis: verum
end;

theorem :: GOBOARD8:17
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k & k + 2 <= len f holds
for j being Element of NAT st 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * (1,(j + 1)) & ( ( f /. k = (GoB f) * (1,(j + 2)) & f /. (k + 2) = (GoB f) * (2,(j + 1)) ) or ( f /. (k + 2) = (GoB f) * (1,(j + 2)) & f /. k = (GoB f) * (2,(j + 1)) ) ) holds
LSeg ((((1 / 2) * (((GoB f) * (1,j)) + ((GoB f) * (1,(j + 1))))) - |[1,0]|),((1 / 2) * (((GoB f) * (1,j)) + ((GoB f) * (2,(j + 1)))))) misses L~ f
proof
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 j being Element of NAT st 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * (1,(j + 1)) & ( ( f /. k = (GoB f) * (1,(j + 2)) & f /. (k + 2) = (GoB f) * (2,(j + 1)) ) or ( f /. (k + 2) = (GoB f) * (1,(j + 2)) & f /. k = (GoB f) * (2,(j + 1)) ) ) holds
LSeg ((((1 / 2) * (((GoB f) * (1,j)) + ((GoB f) * (1,(j + 1))))) - |[1,0]|),((1 / 2) * (((GoB f) * (1,j)) + ((GoB f) * (2,(j + 1)))))) misses L~ f
let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 2 <= len f implies for j being Element of NAT st 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * (1,(j + 1)) & ( ( f /. k = (GoB f) * (1,(j + 2)) & f /. (k + 2) = (GoB f) * (2,(j + 1)) ) or ( f /. (k + 2) = (GoB f) * (1,(j + 2)) & f /. k = (GoB f) * (2,(j + 1)) ) ) holds
LSeg ((((1 / 2) * (((GoB f) * (1,j)) + ((GoB f) * (1,(j + 1))))) - |[1,0]|),((1 / 2) * (((GoB f) * (1,j)) + ((GoB f) * (2,(j + 1)))))) misses L~ f )
assume that
A1: k >= 1 and
A2: k + 2 <= len f ; ::_thesis: for j being Element of NAT st 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * (1,(j + 1)) & ( ( f /. k = (GoB f) * (1,(j + 2)) & f /. (k + 2) = (GoB f) * (2,(j + 1)) ) or ( f /. (k + 2) = (GoB f) * (1,(j + 2)) & f /. k = (GoB f) * (2,(j + 1)) ) ) holds
LSeg ((((1 / 2) * (((GoB f) * (1,j)) + ((GoB f) * (1,(j + 1))))) - |[1,0]|),((1 / 2) * (((GoB f) * (1,j)) + ((GoB f) * (2,(j + 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) = 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 Element of NAT ; ::_thesis: ( 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * (1,(j + 1)) & ( ( f /. k = (GoB f) * (1,(j + 2)) & f /. (k + 2) = (GoB f) * (2,(j + 1)) ) or ( f /. (k + 2) = (GoB f) * (1,(j + 2)) & f /. k = (GoB f) * (2,(j + 1)) ) ) implies LSeg ((((1 / 2) * (((GoB f) * (1,j)) + ((GoB f) * (1,(j + 1))))) - |[1,0]|),((1 / 2) * (((GoB f) * (1,j)) + ((GoB f) * (2,(j + 1)))))) 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 + 2)) & f /. (k + 2) = (GoB f) * (2,(j + 1)) ) or ( f /. (k + 2) = (GoB f) * (1,(j + 2)) & f /. k = (GoB f) * (2,(j + 1)) ) ) ; ::_thesis: LSeg ((((1 / 2) * (((GoB f) * (1,j)) + ((GoB f) * (1,(j + 1))))) - |[1,0]|),((1 / 2) * (((GoB f) * (1,j)) + ((GoB f) * (2,(j + 1)))))) misses L~ f
 (j + 1) + 1 = j + (1 + 1) ;
then A11: j + 1 < width (GoB f) by A8, NAT_1:13;
then A12: j < width (GoB f) by NAT_1:13;
 len (GoB f) <> 0 by GOBOARD1:def_3;
then A13: 0 + 1 <= len (GoB f) by NAT_1:14;
then A14: L~ f misses Int (cell ((GoB f),1,j)) by A12, GOBOARD7:12;
 0 < len (GoB f) by A13, NAT_1:13;
then  L~ f misses Int (cell ((GoB f),0,j)) by A12, GOBOARD7:12;
then A15: L~ f misses (Int (cell ((GoB f),0,j))) \/ (Int (cell ((GoB f),1,j))) by A14, XBOOLE_1:70;
assume  LSeg ((((1 / 2) * (((GoB f) * (1,j)) + ((GoB f) * (1,(j + 1))))) - |[1,0]|),((1 / 2) * (((GoB f) * (1,j)) + ((GoB f) * (2,(j + 1)))))) meets L~ f ; ::_thesis: contradiction
then  L~ f meets ((Int (cell ((GoB f),0,j))) \/ (Int (cell ((GoB f),1,j)))) \/ {((1 / 2) * (((GoB f) * (1,j)) + ((GoB f) * (1,(j + 1)))))} by A7, A6, A12, GOBOARD6:68, XBOOLE_1:63;
then  L~ f meets {((1 / 2) * (((GoB f) * (1,j)) + ((GoB f) * (1,(j + 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) * (1,j))) = LSeg (f,k0) by A7, A9, A13, A11, GOBOARD7:39, ZFMISC_1:50;
A17: ( 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, A11, A6, A16, A17, A4, A5, GOBOARD7:59; ::_thesis: verum
end;

theorem :: GOBOARD8:18
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k & k + 2 <= len f holds
for j being Element of 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
proof
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 j being Element of 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 Element of NAT ; ::_thesis: ( 1 <= k & k + 2 <= len f implies for j being Element of 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 Element of 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 Element of 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 GOBOARD1:def_3;
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, NAT_1:13;
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 Element of 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
end;

theorem :: GOBOARD8:19
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k & k + 2 <= len f holds
for j being Element of NAT st 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * ((len (GoB f)),(j + 1)) & ( ( f /. k = (GoB f) * ((len (GoB f)),(j + 2)) & f /. (k + 2) = (GoB f) * (((len (GoB f)) -' 1),(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((len (GoB f)),(j + 2)) & f /. k = (GoB f) * (((len (GoB f)) -' 1),(j + 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),j)) + ((GoB f) * ((len (GoB f)),(j + 1))))),(((1 / 2) * (((GoB f) * ((len (GoB f)),j)) + ((GoB f) * ((len (GoB f)),(j + 1))))) + |[1,0]|)) misses L~ f
proof
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 j being Element of NAT st 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * ((len (GoB f)),(j + 1)) & ( ( f /. k = (GoB f) * ((len (GoB f)),(j + 2)) & f /. (k + 2) = (GoB f) * (((len (GoB f)) -' 1),(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((len (GoB f)),(j + 2)) & f /. k = (GoB f) * (((len (GoB f)) -' 1),(j + 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),j)) + ((GoB f) * ((len (GoB f)),(j + 1))))),(((1 / 2) * (((GoB f) * ((len (GoB f)),j)) + ((GoB f) * ((len (GoB f)),(j + 1))))) + |[1,0]|)) misses L~ f
let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 2 <= len f implies for j being Element of NAT st 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * ((len (GoB f)),(j + 1)) & ( ( f /. k = (GoB f) * ((len (GoB f)),(j + 2)) & f /. (k + 2) = (GoB f) * (((len (GoB f)) -' 1),(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((len (GoB f)),(j + 2)) & f /. k = (GoB f) * (((len (GoB f)) -' 1),(j + 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),j)) + ((GoB f) * ((len (GoB f)),(j + 1))))),(((1 / 2) * (((GoB f) * ((len (GoB f)),j)) + ((GoB f) * ((len (GoB f)),(j + 1))))) + |[1,0]|)) misses L~ f )
assume that
A1: k >= 1 and
A2: k + 2 <= len f ; ::_thesis: for j being Element of NAT st 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * ((len (GoB f)),(j + 1)) & ( ( f /. k = (GoB f) * ((len (GoB f)),(j + 2)) & f /. (k + 2) = (GoB f) * (((len (GoB f)) -' 1),(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((len (GoB f)),(j + 2)) & f /. k = (GoB f) * (((len (GoB f)) -' 1),(j + 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),j)) + ((GoB f) * ((len (GoB f)),(j + 1))))),(((1 / 2) * (((GoB f) * ((len (GoB f)),j)) + ((GoB f) * ((len (GoB f)),(j + 1))))) + |[1,0]|)) 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 j be Element of NAT ; ::_thesis: ( 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * ((len (GoB f)),(j + 1)) & ( ( f /. k = (GoB f) * ((len (GoB f)),(j + 2)) & f /. (k + 2) = (GoB f) * (((len (GoB f)) -' 1),(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((len (GoB f)),(j + 2)) & f /. k = (GoB f) * (((len (GoB f)) -' 1),(j + 1)) ) ) implies LSeg (((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),j)) + ((GoB f) * ((len (GoB f)),(j + 1))))),(((1 / 2) * (((GoB f) * ((len (GoB f)),j)) + ((GoB f) * ((len (GoB f)),(j + 1))))) + |[1,0]|)) misses L~ f )
assume that
A6: 1 <= j and
A7: j + 2 <= width (GoB f) and
A8: f /. (k + 1) = (GoB f) * ((len (GoB f)),(j + 1)) and
A9: ( ( f /. k = (GoB f) * ((len (GoB f)),(j + 2)) & f /. (k + 2) = (GoB f) * (((len (GoB f)) -' 1),(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((len (GoB f)),(j + 2)) & f /. k = (GoB f) * (((len (GoB f)) -' 1),(j + 1)) ) ) ; ::_thesis: LSeg (((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),j)) + ((GoB f) * ((len (GoB f)),(j + 1))))),(((1 / 2) * (((GoB f) * ((len (GoB f)),j)) + ((GoB f) * ((len (GoB f)),(j + 1))))) + |[1,0]|)) misses L~ f
 (j + 1) + 1 = j + (1 + 1) ;
then A10: j + 1 < width (GoB f) by A7, NAT_1:13;
then A11: j < width (GoB f) by NAT_1:13;
then A12: L~ f misses Int (cell ((GoB f),(len (GoB f)),j)) by GOBOARD7:12;
assume A13: LSeg (((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),j)) + ((GoB f) * ((len (GoB f)),(j + 1))))),(((1 / 2) * (((GoB f) * ((len (GoB f)),j)) + ((GoB f) * ((len (GoB f)),(j + 1))))) + |[1,0]|)) meets L~ f ; ::_thesis: contradiction
A14: 1 < len (GoB f) by GOBOARD7:32;
then A15: ((len (GoB f)) -' 1) + 1 = len (GoB f) by XREAL_1:235;
then A16: (len (GoB f)) -' 1 < len (GoB f) by NAT_1:13;
then  L~ f misses Int (cell ((GoB f),((len (GoB f)) -' 1),j)) by A11, GOBOARD7:12;
then A17: L~ f misses (Int (cell ((GoB f),((len (GoB f)) -' 1),j))) \/ (Int (cell ((GoB f),(len (GoB f)),j))) by A12, XBOOLE_1:70;
A18: 1 <= (len (GoB f)) -' 1 by A14, A15, NAT_1:13;
then  (1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),j)) + ((GoB f) * ((len (GoB f)),(j + 1)))) = (1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),(j + 1))) + ((GoB f) * ((len (GoB f)),j))) by A6, A15, A10, GOBOARD7:9;
then  L~ f meets ((Int (cell ((GoB f),((len (GoB f)) -' 1),j))) \/ (Int (cell ((GoB f),(len (GoB f)),j)))) \/ {((1 / 2) * (((GoB f) * ((len (GoB f)),j)) + ((GoB f) * ((len (GoB f)),(j + 1)))))} by A6, A14, A11, A13, GOBOARD6:69, XBOOLE_1:63;
then  L~ f meets {((1 / 2) * (((GoB f) * ((len (GoB f)),j)) + ((GoB f) * ((len (GoB f)),(j + 1)))))} by A17, XBOOLE_1:70;
then consider k0 being Element of NAT  such that
 1 <= k0 and
 k0 + 1 <= len f and
A19: LSeg ((f /. (k + 1)),((GoB f) * ((len (GoB f)),j))) = LSeg (f,k0) by A6, A8, A14, A10, GOBOARD7:39, ZFMISC_1:50;
 ( LSeg (f,k0) c= L~ f & LSeg (f,k) c= L~ f ) by TOPREAL3:19;
hence  contradiction by A6, A8, A9, A15, A18, A16, A10, A19, A4, A5, GOBOARD7:60; ::_thesis: verum
end;

theorem :: GOBOARD8:20
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k & k + 2 <= len f holds
for j being Element of NAT st 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * ((len (GoB f)),(j + 1)) & ( ( f /. k = (GoB f) * ((len (GoB f)),j) & f /. (k + 2) = (GoB f) * (((len (GoB f)) -' 1),(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((len (GoB f)),j) & f /. k = (GoB f) * (((len (GoB f)) -' 1),(j + 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),(j + 1))) + ((GoB f) * ((len (GoB f)),(j + 2))))),(((1 / 2) * (((GoB f) * ((len (GoB f)),(j + 1))) + ((GoB f) * ((len (GoB f)),(j + 2))))) + |[1,0]|)) misses L~ f
proof
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 j being Element of NAT st 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * ((len (GoB f)),(j + 1)) & ( ( f /. k = (GoB f) * ((len (GoB f)),j) & f /. (k + 2) = (GoB f) * (((len (GoB f)) -' 1),(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((len (GoB f)),j) & f /. k = (GoB f) * (((len (GoB f)) -' 1),(j + 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),(j + 1))) + ((GoB f) * ((len (GoB f)),(j + 2))))),(((1 / 2) * (((GoB f) * ((len (GoB f)),(j + 1))) + ((GoB f) * ((len (GoB f)),(j + 2))))) + |[1,0]|)) misses L~ f
let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 2 <= len f implies for j being Element of NAT st 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * ((len (GoB f)),(j + 1)) & ( ( f /. k = (GoB f) * ((len (GoB f)),j) & f /. (k + 2) = (GoB f) * (((len (GoB f)) -' 1),(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((len (GoB f)),j) & f /. k = (GoB f) * (((len (GoB f)) -' 1),(j + 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),(j + 1))) + ((GoB f) * ((len (GoB f)),(j + 2))))),(((1 / 2) * (((GoB f) * ((len (GoB f)),(j + 1))) + ((GoB f) * ((len (GoB f)),(j + 2))))) + |[1,0]|)) misses L~ f )
assume that
A1: k >= 1 and
A2: k + 2 <= len f ; ::_thesis: for j being Element of NAT st 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * ((len (GoB f)),(j + 1)) & ( ( f /. k = (GoB f) * ((len (GoB f)),j) & f /. (k + 2) = (GoB f) * (((len (GoB f)) -' 1),(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((len (GoB f)),j) & f /. k = (GoB f) * (((len (GoB f)) -' 1),(j + 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),(j + 1))) + ((GoB f) * ((len (GoB f)),(j + 2))))),(((1 / 2) * (((GoB f) * ((len (GoB f)),(j + 1))) + ((GoB f) * ((len (GoB f)),(j + 2))))) + |[1,0]|)) 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 j be Element of NAT ; ::_thesis: ( 1 <= j & j + 2 <= width (GoB f) & f /. (k + 1) = (GoB f) * ((len (GoB f)),(j + 1)) & ( ( f /. k = (GoB f) * ((len (GoB f)),j) & f /. (k + 2) = (GoB f) * (((len (GoB f)) -' 1),(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((len (GoB f)),j) & f /. k = (GoB f) * (((len (GoB f)) -' 1),(j + 1)) ) ) implies LSeg (((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),(j + 1))) + ((GoB f) * ((len (GoB f)),(j + 2))))),(((1 / 2) * (((GoB f) * ((len (GoB f)),(j + 1))) + ((GoB f) * ((len (GoB f)),(j + 2))))) + |[1,0]|)) misses L~ f )
assume that
A6: 1 <= j and
A7: j + 2 <= width (GoB f) and
A8: f /. (k + 1) = (GoB f) * ((len (GoB f)),(j + 1)) and
A9: ( ( f /. k = (GoB f) * ((len (GoB f)),j) & f /. (k + 2) = (GoB f) * (((len (GoB f)) -' 1),(j + 1)) ) or ( f /. (k + 2) = (GoB f) * ((len (GoB f)),j) & f /. k = (GoB f) * (((len (GoB f)) -' 1),(j + 1)) ) ) ; ::_thesis: LSeg (((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),(j + 1))) + ((GoB f) * ((len (GoB f)),(j + 2))))),(((1 / 2) * (((GoB f) * ((len (GoB f)),(j + 1))) + ((GoB f) * ((len (GoB f)),(j + 2))))) + |[1,0]|)) misses L~ f
A10: (j + 1) + 1 = j + (1 + 1) ;
then A11: j + 1 < width (GoB f) by A7, NAT_1:13;
then A12: L~ f misses Int (cell ((GoB f),(len (GoB f)),(j + 1))) by GOBOARD7:12;
A13: 1 <= len (GoB f) by GOBOARD7:32;
then A14: ((len (GoB f)) -' 1) + 1 = len (GoB f) by XREAL_1:235;
then A15: (len (GoB f)) -' 1 < len (GoB f) by NAT_1:13;
then  L~ f misses Int (cell ((GoB f),((len (GoB f)) -' 1),(j + 1))) by A11, GOBOARD7:12;
then A16: L~ f misses (Int (cell ((GoB f),((len (GoB f)) -' 1),(j + 1)))) \/ (Int (cell ((GoB f),(len (GoB f)),(j + 1)))) by A12, XBOOLE_1:70;
assume A17: LSeg (((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),(j + 1))) + ((GoB f) * ((len (GoB f)),(j + 2))))),(((1 / 2) * (((GoB f) * ((len (GoB f)),(j + 1))) + ((GoB f) * ((len (GoB f)),(j + 2))))) + |[1,0]|)) meets L~ f ; ::_thesis: contradiction
A18: 1 <= j + 1 by NAT_1:11;
A19: 1 < len (GoB f) by GOBOARD7:32;
then A20: 1 <= (len (GoB f)) -' 1 by A14, NAT_1:13;
then  (1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),(j + 1))) + ((GoB f) * ((len (GoB f)),(j + 2)))) = (1 / 2) * (((GoB f) * ((len (GoB f)),(j + 1))) + ((GoB f) * (((len (GoB f)) -' 1),(j + 2)))) by A7, A14, A10, A18, GOBOARD7:9;
then  L~ f meets ((Int (cell ((GoB f),((len (GoB f)) -' 1),(j + 1)))) \/ (Int (cell ((GoB f),(len (GoB f)),(j + 1))))) \/ {((1 / 2) * (((GoB f) * ((len (GoB f)),(j + 1))) + ((GoB f) * ((len (GoB f)),(j + 2)))))} by A19, A10, A11, A18, A17, GOBOARD6:69, XBOOLE_1:63;
then  L~ f meets {((1 / 2) * (((GoB f) * ((len (GoB f)),(j + 1))) + ((GoB f) * ((len (GoB f)),(j + 2)))))} 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) * ((len (GoB f)),(j + 2)))) = LSeg (f,k0) by A7, A8, A13, A10, A18, GOBOARD7:39, ZFMISC_1:50;
 ( LSeg (f,k0) c= L~ f & LSeg (f,k) c= L~ f ) by TOPREAL3:19;
hence  contradiction by A6, A8, A9, A14, A20, A15, A11, A21, A4, A5, GOBOARD7:60; ::_thesis: verum
end;

theorem Th21: :: GOBOARD8:21
for f being non constant standard special_circular_sequence
for P being Subset of (TOP-REAL 2) st ( for p being Point of (TOP-REAL 2) st p in P holds
p `1 < ((GoB f) * (1,1)) `1 ) holds
P misses L~ f
proof
let f be non constant standard special_circular_sequence; ::_thesis: for P being Subset of (TOP-REAL 2) st ( for p being Point of (TOP-REAL 2) st p in P holds
p `1 < ((GoB f) * (1,1)) `1 ) holds
P misses L~ f
let P be Subset of (TOP-REAL 2); ::_thesis: ( ( for p being Point of (TOP-REAL 2) st p in P holds
p `1 < ((GoB f) * (1,1)) `1 ) implies P misses L~ f )
assume A1: for p being Point of (TOP-REAL 2) st p in P holds
p `1 < ((GoB f) * (1,1)) `1 ; ::_thesis: P misses L~ f
assume  P meets L~ f ; ::_thesis: contradiction
then consider x being set  such that
A2: x in P and
A3: x in L~ f by XBOOLE_0:3;
reconsider x = x as Point of (TOP-REAL 2) by A2;
A4: x `1 < ((GoB f) * (1,1)) `1 by A1, A2;
A5: 1 < width (GoB f) by GOBOARD7:33;
A6: f is_sequence_on GoB f by GOBOARD5:def_5;
consider i being Element of NAT  such that
A7: 1 <= i and
A8: i + 1 <= len f and
A9: x in LSeg ((f /. i),(f /. (i + 1))) by A3, SPPOL_2:14;
percases ( (f /. i) `1 <= (f /. (i + 1)) `1 or (f /. i) `1 >= (f /. (i + 1)) `1 ) ;
suppose (f /. i) `1 <= (f /. (i + 1)) `1 ; ::_thesis: contradiction
then A10: (f /. i) `1 <= x `1 by A9, TOPREAL1:3;
 i <= len f by A8, NAT_1:13;
then  i in dom f by A7, FINSEQ_3:25;
then consider i1, j1 being Element of NAT  such that
A11: [i1,j1] in Indices (GoB f) and
A12: f /. i = (GoB f) * (i1,j1) by A6, GOBOARD1:def_9;
A13: 1 <= i1 by A11, MATRIX_1:38;
A14: i1 <= len (GoB f) by A11, MATRIX_1:38;
 ( 1 <= j1 & j1 <= width (GoB f) ) by A11, MATRIX_1:38;
then A15: (f /. i) `1 = ((GoB f) * (i1,1)) `1 by A12, A13, A14, GOBOARD5:2;
then  1 < i1 by A4, A10, A13, XXREAL_0:1;
then  ((GoB f) * (1,1)) `1 < (f /. i) `1 by A5, A14, A15, GOBOARD5:3;
hence  contradiction by A1, A2, A10, XXREAL_0:2; ::_thesis: verum
end;
suppose (f /. i) `1 >= (f /. (i + 1)) `1 ; ::_thesis: contradiction
then A16: (f /. (i + 1)) `1 <= x `1 by A9, TOPREAL1:3;
 1 <= i + 1 by NAT_1:11;
then  i + 1 in dom f by A8, FINSEQ_3:25;
then consider i1, j1 being Element of NAT  such that
A17: [i1,j1] in Indices (GoB f) and
A18: f /. (i + 1) = (GoB f) * (i1,j1) by A6, GOBOARD1:def_9;
A19: 1 <= i1 by A17, MATRIX_1:38;
A20: i1 <= len (GoB f) by A17, MATRIX_1:38;
 ( 1 <= j1 & j1 <= width (GoB f) ) by A17, MATRIX_1:38;
then A21: (f /. (i + 1)) `1 = ((GoB f) * (i1,1)) `1 by A18, A19, A20, GOBOARD5:2;
then  1 < i1 by A4, A16, A19, XXREAL_0:1;
then  ((GoB f) * (1,1)) `1 < (f /. (i + 1)) `1 by A5, A20, A21, GOBOARD5:3;
hence  contradiction by A1, A2, A16, XXREAL_0:2; ::_thesis: verum
end;
end;
end;

theorem Th22: :: GOBOARD8:22
for f being non constant standard special_circular_sequence
for P being Subset of (TOP-REAL 2) st ( for p being Point of (TOP-REAL 2) st p in P holds
p `1 > ((GoB f) * ((len (GoB f)),1)) `1 ) holds
P misses L~ f
proof
let f be non constant standard special_circular_sequence; ::_thesis: for P being Subset of (TOP-REAL 2) st ( for p being Point of (TOP-REAL 2) st p in P holds
p `1 > ((GoB f) * ((len (GoB f)),1)) `1 ) holds
P misses L~ f
let P be Subset of (TOP-REAL 2); ::_thesis: ( ( for p being Point of (TOP-REAL 2) st p in P holds
p `1 > ((GoB f) * ((len (GoB f)),1)) `1 ) implies P misses L~ f )
assume A1: for p being Point of (TOP-REAL 2) st p in P holds
p `1 > ((GoB f) * ((len (GoB f)),1)) `1 ; ::_thesis: P misses L~ f
assume  P meets L~ f ; ::_thesis: contradiction
then consider x being set  such that
A2: x in P and
A3: x in L~ f by XBOOLE_0:3;
reconsider x = x as Point of (TOP-REAL 2) by A2;
A4: x `1 > ((GoB f) * ((len (GoB f)),1)) `1 by A1, A2;
A5: 1 < width (GoB f) by GOBOARD7:33;
A6: f is_sequence_on GoB f by GOBOARD5:def_5;
consider i being Element of NAT  such that
A7: 1 <= i and
A8: i + 1 <= len f and
A9: x in LSeg ((f /. i),(f /. (i + 1))) by A3, SPPOL_2:14;
percases ( (f /. i) `1 >= (f /. (i + 1)) `1 or (f /. i) `1 <= (f /. (i + 1)) `1 ) ;
suppose (f /. i) `1 >= (f /. (i + 1)) `1 ; ::_thesis: contradiction
then A10: (f /. i) `1 >= x `1 by A9, TOPREAL1:3;
 i <= len f by A8, NAT_1:13;
then  i in dom f by A7, FINSEQ_3:25;
then consider i1, j1 being Element of NAT  such that
A11: [i1,j1] in Indices (GoB f) and
A12: f /. i = (GoB f) * (i1,j1) by A6, GOBOARD1:def_9;
A13: 1 <= i1 by A11, MATRIX_1:38;
A14: i1 <= len (GoB f) by A11, MATRIX_1:38;
 ( 1 <= j1 & j1 <= width (GoB f) ) by A11, MATRIX_1:38;
then A15: (f /. i) `1 = ((GoB f) * (i1,1)) `1 by A12, A13, A14, GOBOARD5:2;
then  i1 < len (GoB f) by A4, A10, A14, XXREAL_0:1;
then  ((GoB f) * ((len (GoB f)),1)) `1 > (f /. i) `1 by A5, A13, A15, GOBOARD5:3;
hence  contradiction by A1, A2, A10, XXREAL_0:2; ::_thesis: verum
end;
suppose (f /. i) `1 <= (f /. (i + 1)) `1 ; ::_thesis: contradiction
then A16: (f /. (i + 1)) `1 >= x `1 by A9, TOPREAL1:3;
 1 <= i + 1 by NAT_1:11;
then  i + 1 in dom f by A8, FINSEQ_3:25;
then consider i1, j1 being Element of NAT  such that
A17: [i1,j1] in Indices (GoB f) and
A18: f /. (i + 1) = (GoB f) * (i1,j1) by A6, GOBOARD1:def_9;
A19: 1 <= i1 by A17, MATRIX_1:38;
A20: i1 <= len (GoB f) by A17, MATRIX_1:38;
 ( 1 <= j1 & j1 <= width (GoB f) ) by A17, MATRIX_1:38;
then A21: (f /. (i + 1)) `1 = ((GoB f) * (i1,1)) `1 by A18, A19, A20, GOBOARD5:2;
then  i1 < len (GoB f) by A4, A16, A20, XXREAL_0:1;
then  ((GoB f) * ((len (GoB f)),1)) `1 > (f /. (i + 1)) `1 by A5, A19, A21, GOBOARD5:3;
hence  contradiction by A1, A2, A16, XXREAL_0:2; ::_thesis: verum
end;
end;
end;

theorem Th23: :: GOBOARD8:23
for f being non constant standard special_circular_sequence
for P being Subset of (TOP-REAL 2) st ( for p being Point of (TOP-REAL 2) st p in P holds
p `2 < ((GoB f) * (1,1)) `2 ) holds
P misses L~ f
proof
let f be non constant standard special_circular_sequence; ::_thesis: for P being Subset of (TOP-REAL 2) st ( for p being Point of (TOP-REAL 2) st p in P holds
p `2 < ((GoB f) * (1,1)) `2 ) holds
P misses L~ f
let P be Subset of (TOP-REAL 2); ::_thesis: ( ( for p being Point of (TOP-REAL 2) st p in P holds
p `2 < ((GoB f) * (1,1)) `2 ) implies P misses L~ f )
assume A1: for p being Point of (TOP-REAL 2) st p in P holds
p `2 < ((GoB f) * (1,1)) `2 ; ::_thesis: P misses L~ f
assume  P meets L~ f ; ::_thesis: contradiction
then consider x being set  such that
A2: x in P and
A3: x in L~ f by XBOOLE_0:3;
reconsider x = x as Point of (TOP-REAL 2) by A2;
A4: x `2 < ((GoB f) * (1,1)) `2 by A1, A2;
A5: 1 < len (GoB f) by GOBOARD7:32;
A6: f is_sequence_on GoB f by GOBOARD5:def_5;
consider j being Element of NAT  such that
A7: 1 <= j and
A8: j + 1 <= len f and
A9: x in LSeg ((f /. j),(f /. (j + 1))) by A3, SPPOL_2:14;
percases ( (f /. j) `2 <= (f /. (j + 1)) `2 or (f /. j) `2 >= (f /. (j + 1)) `2 ) ;
suppose (f /. j) `2 <= (f /. (j + 1)) `2 ; ::_thesis: contradiction
then A10: (f /. j) `2 <= x `2 by A9, TOPREAL1:4;
 j <= len f by A8, NAT_1:13;
then  j in dom f by A7, FINSEQ_3:25;
then consider i1, j1 being Element of NAT  such that
A11: [i1,j1] in Indices (GoB f) and
A12: f /. j = (GoB f) * (i1,j1) by A6, GOBOARD1:def_9;
A13: 1 <= j1 by A11, MATRIX_1:38;
A14: j1 <= width (GoB f) by A11, MATRIX_1:38;
 ( 1 <= i1 & i1 <= len (GoB f) ) by A11, MATRIX_1:38;
then A15: (f /. j) `2 = ((GoB f) * (1,j1)) `2 by A12, A13, A14, GOBOARD5:1;
then  1 < j1 by A4, A10, A13, XXREAL_0:1;
then  ((GoB f) * (1,1)) `2 < (f /. j) `2 by A5, A14, A15, GOBOARD5:4;
hence  contradiction by A1, A2, A10, XXREAL_0:2; ::_thesis: verum
end;
suppose (f /. j) `2 >= (f /. (j + 1)) `2 ; ::_thesis: contradiction
then A16: (f /. (j + 1)) `2 <= x `2 by A9, TOPREAL1:4;
 1 <= j + 1 by NAT_1:11;
then  j + 1 in dom f by A8, FINSEQ_3:25;
then consider i1, j1 being Element of NAT  such that
A17: [i1,j1] in Indices (GoB f) and
A18: f /. (j + 1) = (GoB f) * (i1,j1) by A6, GOBOARD1:def_9;
A19: 1 <= j1 by A17, MATRIX_1:38;
A20: j1 <= width (GoB f) by A17, MATRIX_1:38;
 ( 1 <= i1 & i1 <= len (GoB f) ) by A17, MATRIX_1:38;
then A21: (f /. (j + 1)) `2 = ((GoB f) * (1,j1)) `2 by A18, A19, A20, GOBOARD5:1;
then  1 < j1 by A4, A16, A19, XXREAL_0:1;
then  ((GoB f) * (1,1)) `2 < (f /. (j + 1)) `2 by A5, A20, A21, GOBOARD5:4;
hence  contradiction by A1, A2, A16, XXREAL_0:2; ::_thesis: verum
end;
end;
end;

theorem Th24: :: GOBOARD8:24
for f being non constant standard special_circular_sequence
for P being Subset of (TOP-REAL 2) st ( for p being Point of (TOP-REAL 2) st p in P holds
p `2 > ((GoB f) * (1,(width (GoB f)))) `2 ) holds
P misses L~ f
proof
let f be non constant standard special_circular_sequence; ::_thesis: for P being Subset of (TOP-REAL 2) st ( for p being Point of (TOP-REAL 2) st p in P holds
p `2 > ((GoB f) * (1,(width (GoB f)))) `2 ) holds
P misses L~ f
let P be Subset of (TOP-REAL 2); ::_thesis: ( ( for p being Point of (TOP-REAL 2) st p in P holds
p `2 > ((GoB f) * (1,(width (GoB f)))) `2 ) implies P misses L~ f )
assume A1: for p being Point of (TOP-REAL 2) st p in P holds
p `2 > ((GoB f) * (1,(width (GoB f)))) `2 ; ::_thesis: P misses L~ f
assume  P meets L~ f ; ::_thesis: contradiction
then consider x being set  such that
A2: x in P and
A3: x in L~ f by XBOOLE_0:3;
reconsider x = x as Point of (TOP-REAL 2) by A2;
A4: x `2 > ((GoB f) * (1,(width (GoB f)))) `2 by A1, A2;
A5: 1 < len (GoB f) by GOBOARD7:32;
A6: f is_sequence_on GoB f by GOBOARD5:def_5;
consider j being Element of NAT  such that
A7: 1 <= j and
A8: j + 1 <= len f and
A9: x in LSeg ((f /. j),(f /. (j + 1))) by A3, SPPOL_2:14;
percases ( (f /. j) `2 >= (f /. (j + 1)) `2 or (f /. j) `2 <= (f /. (j + 1)) `2 ) ;
suppose (f /. j) `2 >= (f /. (j + 1)) `2 ; ::_thesis: contradiction
then A10: (f /. j) `2 >= x `2 by A9, TOPREAL1:4;
 j <= len f by A8, NAT_1:13;
then  j in dom f by A7, FINSEQ_3:25;
then consider i1, j1 being Element of NAT  such that
A11: [i1,j1] in Indices (GoB f) and
A12: f /. j = (GoB f) * (i1,j1) by A6, GOBOARD1:def_9;
A13: 1 <= j1 by A11, MATRIX_1:38;
A14: j1 <= width (GoB f) by A11, MATRIX_1:38;
 ( 1 <= i1 & i1 <= len (GoB f) ) by A11, MATRIX_1:38;
then A15: (f /. j) `2 = ((GoB f) * (1,j1)) `2 by A12, A13, A14, GOBOARD5:1;
then  j1 < width (GoB f) by A4, A10, A14, XXREAL_0:1;
then  ((GoB f) * (1,(width (GoB f)))) `2 > (f /. j) `2 by A5, A13, A15, GOBOARD5:4;
hence  contradiction by A1, A2, A10, XXREAL_0:2; ::_thesis: verum
end;
suppose (f /. j) `2 <= (f /. (j + 1)) `2 ; ::_thesis: contradiction
then A16: (f /. (j + 1)) `2 >= x `2 by A9, TOPREAL1:4;
 1 <= j + 1 by NAT_1:11;
then  j + 1 in dom f by A8, FINSEQ_3:25;
then consider i1, j1 being Element of NAT  such that
A17: [i1,j1] in Indices (GoB f) and
A18: f /. (j + 1) = (GoB f) * (i1,j1) by A6, GOBOARD1:def_9;
A19: 1 <= j1 by A17, MATRIX_1:38;
A20: j1 <= width (GoB f) by A17, MATRIX_1:38;
 ( 1 <= i1 & i1 <= len (GoB f) ) by A17, MATRIX_1:38;
then A21: (f /. (j + 1)) `2 = ((GoB f) * (1,j1)) `2 by A18, A19, A20, GOBOARD5:1;
then  j1 < width (GoB f) by A4, A16, A20, XXREAL_0:1;
then  ((GoB f) * (1,(width (GoB f)))) `2 > (f /. (j + 1)) `2 by A5, A19, A21, GOBOARD5:4;
hence  contradiction by A1, A2, A16, XXREAL_0:2; ::_thesis: verum
end;
end;
end;

theorem :: GOBOARD8:25
for f being non constant standard special_circular_sequence
for i being Element of NAT st 1 <= i & i + 2 <= len (GoB f) holds
LSeg ((((1 / 2) * (((GoB f) * (i,1)) + ((GoB f) * ((i + 1),1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * ((i + 1),1)) + ((GoB f) * ((i + 2),1)))) - |[0,1]|)) misses L~ f
proof
let f be non constant standard special_circular_sequence; ::_thesis: for i being Element of NAT st 1 <= i & i + 2 <= len (GoB f) holds
LSeg ((((1 / 2) * (((GoB f) * (i,1)) + ((GoB f) * ((i + 1),1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * ((i + 1),1)) + ((GoB f) * ((i + 2),1)))) - |[0,1]|)) misses L~ f
let i be Element of NAT ; ::_thesis: ( 1 <= i & i + 2 <= len (GoB f) implies LSeg ((((1 / 2) * (((GoB f) * (i,1)) + ((GoB f) * ((i + 1),1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * ((i + 1),1)) + ((GoB f) * ((i + 2),1)))) - |[0,1]|)) misses L~ f )
assume that
A1: 1 <= i and
A2: i + 2 <= len (GoB f) ; ::_thesis: LSeg ((((1 / 2) * (((GoB f) * (i,1)) + ((GoB f) * ((i + 1),1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * ((i + 1),1)) + ((GoB f) * ((i + 2),1)))) - |[0,1]|)) misses L~ f
A3: 1 <= width (GoB f) by GOBOARD7:33;
now__::_thesis:_for_p_being_Point_of_(TOP-REAL_2)_st_p_in_LSeg_((((1_/_2)_*_(((GoB_f)_*_(i,1))_+_((GoB_f)_*_((i_+_1),1))))_-_|[0,1]|),(((1_/_2)_*_(((GoB_f)_*_((i_+_1),1))_+_((GoB_f)_*_((i_+_2),1))))_-_|[0,1]|))_holds_
p_`2_<_((GoB_f)_*_(1,1))_`2
A4: i <= i + 2 by NAT_1:11;
then  i <= len (GoB f) by A2, XXREAL_0:2;
then A5: ((GoB f) * (i,1)) `2 = ((GoB f) * (1,1)) `2 by A1, A3, GOBOARD5:1;
 i + 1 <= i + 2 by XREAL_1:6;
then  ( 1 <= i + 1 & i + 1 <= len (GoB f) ) by A2, NAT_1:11, XXREAL_0:2;
then A6: ((GoB f) * ((i + 1),1)) `2 = ((GoB f) * (1,1)) `2 by A3, GOBOARD5:1;
 1 <= i + 2 by A1, A4, XXREAL_0:2;
then A7: ((GoB f) * ((i + 2),1)) `2 = ((GoB f) * (1,1)) `2 by A2, A3, GOBOARD5:1;
(((1 / 2) * (((GoB f) * ((i + 1),1)) + ((GoB f) * ((i + 2),1)))) - |[0,1]|) `2 = (((1 / 2) * (((GoB f) * ((i + 1),1)) + ((GoB f) * ((i + 2),1)))) `2) - (|[0,1]| `2) by TOPREAL3:3
.= ((1 / 2) * ((((GoB f) * ((i + 1),1)) + ((GoB f) * ((i + 2),1))) `2)) - (|[0,1]| `2) by TOPREAL3:4
.= ((1 / 2) * ((((GoB f) * (1,1)) `2) + (((GoB f) * (1,1)) `2))) - (|[0,1]| `2) by A6, A7, TOPREAL3:2
.= (1 * (((GoB f) * (1,1)) `2)) - 1 by EUCLID:52 ;
then A8: ((1 / 2) * (((GoB f) * ((i + 1),1)) + ((GoB f) * ((i + 2),1)))) - |[0,1]| = |[((((1 / 2) * (((GoB f) * ((i + 1),1)) + ((GoB f) * ((i + 2),1)))) - |[0,1]|) `1),((((GoB f) * (1,1)) `2) - 1)]| by EUCLID:53;
(((1 / 2) * (((GoB f) * (i,1)) + ((GoB f) * ((i + 1),1)))) - |[0,1]|) `2 = (((1 / 2) * (((GoB f) * (i,1)) + ((GoB f) * ((i + 1),1)))) `2) - (|[0,1]| `2) by TOPREAL3:3
.= ((1 / 2) * ((((GoB f) * (i,1)) + ((GoB f) * ((i + 1),1))) `2)) - (|[0,1]| `2) by TOPREAL3:4
.= ((1 / 2) * ((((GoB f) * (1,1)) `2) + (((GoB f) * (1,1)) `2))) - (|[0,1]| `2) by A5, A6, TOPREAL3:2
.= (1 * (((GoB f) * (1,1)) `2)) - 1 by EUCLID:52 ;
then A9: ((1 / 2) * (((GoB f) * (i,1)) + ((GoB f) * ((i + 1),1)))) - |[0,1]| = |[((((1 / 2) * (((GoB f) * (i,1)) + ((GoB f) * ((i + 1),1)))) - |[0,1]|) `1),((((GoB f) * (1,1)) `2) - 1)]| by EUCLID:53;
let p be Point of (TOP-REAL 2); ::_thesis: ( p in LSeg ((((1 / 2) * (((GoB f) * (i,1)) + ((GoB f) * ((i + 1),1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * ((i + 1),1)) + ((GoB f) * ((i + 2),1)))) - |[0,1]|)) implies p `2 < ((GoB f) * (1,1)) `2 )
assume  p in LSeg ((((1 / 2) * (((GoB f) * (i,1)) + ((GoB f) * ((i + 1),1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * ((i + 1),1)) + ((GoB f) * ((i + 2),1)))) - |[0,1]|)) ; ::_thesis: p `2 < ((GoB f) * (1,1)) `2
then  p `2 = (((GoB f) * (1,1)) `2) - 1 by A9, A8, TOPREAL3:12;
hence  p `2 < ((GoB f) * (1,1)) `2 by XREAL_1:44; ::_thesis: verum
end;
hence  LSeg ((((1 / 2) * (((GoB f) * (i,1)) + ((GoB f) * ((i + 1),1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * ((i + 1),1)) + ((GoB f) * ((i + 2),1)))) - |[0,1]|)) misses L~ f by Th23; ::_thesis: verum
end;

theorem :: GOBOARD8:26
for f being non constant standard special_circular_sequence holds LSeg ((((GoB f) * (1,1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,1)))) - |[0,1]|)) misses L~ f
proof
let f be non constant standard special_circular_sequence; ::_thesis: LSeg ((((GoB f) * (1,1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,1)))) - |[0,1]|)) misses L~ f
A1: 1 <= width (GoB f) by GOBOARD7:33;
now__::_thesis:_for_p_being_Point_of_(TOP-REAL_2)_st_p_in_LSeg_((((GoB_f)_*_(1,1))_-_|[1,1]|),(((1_/_2)_*_(((GoB_f)_*_(1,1))_+_((GoB_f)_*_(2,1))))_-_|[0,1]|))_holds_
p_`2_<_((GoB_f)_*_(1,1))_`2
 1 < len (GoB f) by GOBOARD7:32;
then  1 + 1 <= len (GoB f) by NAT_1:13;
then A2: ((GoB f) * (2,1)) `2 = ((GoB f) * (1,1)) `2 by A1, GOBOARD5:1;
(((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,1)))) - |[0,1]|) `2 = (((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,1)))) `2) - (|[0,1]| `2) by TOPREAL3:3
.= ((1 / 2) * ((((GoB f) * (1,1)) + ((GoB f) * (2,1))) `2)) - (|[0,1]| `2) by TOPREAL3:4
.= ((1 / 2) * ((((GoB f) * (1,1)) `2) + (((GoB f) * (1,1)) `2))) - (|[0,1]| `2) by A2, TOPREAL3:2
.= (1 * (((GoB f) * (1,1)) `2)) - 1 by EUCLID:52 ;
then A3: ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,1)))) - |[0,1]| = |[((((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,1)))) - |[0,1]|) `1),((((GoB f) * (1,1)) `2) - 1)]| by EUCLID:53;
(((GoB f) * (1,1)) - |[1,1]|) `2 = (((GoB f) * (1,1)) `2) - (|[1,1]| `2) by TOPREAL3:3
.= (((GoB f) * (1,1)) `2) - 1 by EUCLID:52 ;
then A4: ((GoB f) * (1,1)) - |[1,1]| = |[((((GoB f) * (1,1)) - |[1,1]|) `1),((((GoB f) * (1,1)) `2) - 1)]| by EUCLID:53;
let p be Point of (TOP-REAL 2); ::_thesis: ( p in LSeg ((((GoB f) * (1,1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,1)))) - |[0,1]|)) implies p `2 < ((GoB f) * (1,1)) `2 )
assume  p in LSeg ((((GoB f) * (1,1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,1)))) - |[0,1]|)) ; ::_thesis: p `2 < ((GoB f) * (1,1)) `2
then  p `2 = (((GoB f) * (1,1)) `2) - 1 by A4, A3, TOPREAL3:12;
hence  p `2 < ((GoB f) * (1,1)) `2 by XREAL_1:44; ::_thesis: verum
end;
hence  LSeg ((((GoB f) * (1,1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (2,1)))) - |[0,1]|)) misses L~ f by Th23; ::_thesis: verum
end;

theorem :: GOBOARD8:27
for f being non constant standard special_circular_sequence holds LSeg ((((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1)))) - |[0,1]|),(((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|)) misses L~ f
proof
let f be non constant standard special_circular_sequence; ::_thesis: LSeg ((((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1)))) - |[0,1]|),(((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|)) misses L~ f
A1: 1 <= width (GoB f) by GOBOARD7:33;
now__::_thesis:_for_p_being_Point_of_(TOP-REAL_2)_st_p_in_LSeg_((((1_/_2)_*_(((GoB_f)_*_(((len_(GoB_f))_-'_1),1))_+_((GoB_f)_*_((len_(GoB_f)),1))))_-_|[0,1]|),(((GoB_f)_*_((len_(GoB_f)),1))_+_|[1,(-_1)]|))_holds_
p_`2_<_((GoB_f)_*_(1,1))_`2
A2: 1 < len (GoB f) by GOBOARD7:32;
then A3: ((len (GoB f)) -' 1) + 1 = len (GoB f) by XREAL_1:235;
then A4: (len (GoB f)) -' 1 <= len (GoB f) by NAT_1:11;
A5: ((GoB f) * ((len (GoB f)),1)) `2 = ((GoB f) * (1,1)) `2 by A1, A2, GOBOARD5:1;
then (((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|) `2 = (((GoB f) * (1,1)) `2) + (|[1,(- 1)]| `2) by TOPREAL3:2
.= (((GoB f) * (1,1)) `2) + (- 1) by EUCLID:52
.= (((GoB f) * (1,1)) `2) - 1 ;
then A6: ((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]| = |[((((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|) `1),((((GoB f) * (1,1)) `2) - 1)]| by EUCLID:53;
 1 <= (len (GoB f)) -' 1 by A2, A3, NAT_1:13;
then A7: ((GoB f) * (((len (GoB f)) -' 1),1)) `2 = ((GoB f) * (1,1)) `2 by A1, A4, GOBOARD5:1;
(((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1)))) - |[0,1]|) `2 = (((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1)))) `2) - (|[0,1]| `2) by TOPREAL3:3
.= ((1 / 2) * ((((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1))) `2)) - (|[0,1]| `2) by TOPREAL3:4
.= ((1 / 2) * ((((GoB f) * (1,1)) `2) + (((GoB f) * (1,1)) `2))) - (|[0,1]| `2) by A7, A5, TOPREAL3:2
.= (1 * (((GoB f) * (1,1)) `2)) - 1 by EUCLID:52 ;
then A8: ((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1)))) - |[0,1]| = |[((((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1)))) - |[0,1]|) `1),((((GoB f) * (1,1)) `2) - 1)]| by EUCLID:53;
let p be Point of (TOP-REAL 2); ::_thesis: ( p in LSeg ((((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1)))) - |[0,1]|),(((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|)) implies p `2 < ((GoB f) * (1,1)) `2 )
assume  p in LSeg ((((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1)))) - |[0,1]|),(((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|)) ; ::_thesis: p `2 < ((GoB f) * (1,1)) `2
then  p `2 = (((GoB f) * (1,1)) `2) - 1 by A8, A6, TOPREAL3:12;
hence  p `2 < ((GoB f) * (1,1)) `2 by XREAL_1:44; ::_thesis: verum
end;
hence  LSeg ((((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1)))) - |[0,1]|),(((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|)) misses L~ f by Th23; ::_thesis: verum
end;

theorem :: GOBOARD8:28
for f being non constant standard special_circular_sequence
for i being Element of NAT st 1 <= i & i + 2 <= len (GoB f) holds
LSeg ((((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|),(((1 / 2) * (((GoB f) * ((i + 1),(width (GoB f)))) + ((GoB f) * ((i + 2),(width (GoB f)))))) + |[0,1]|)) misses L~ f
proof
let f be non constant standard special_circular_sequence; ::_thesis: for i being Element of NAT st 1 <= i & i + 2 <= len (GoB f) holds
LSeg ((((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|),(((1 / 2) * (((GoB f) * ((i + 1),(width (GoB f)))) + ((GoB f) * ((i + 2),(width (GoB f)))))) + |[0,1]|)) misses L~ f
let i be Element of NAT ; ::_thesis: ( 1 <= i & i + 2 <= len (GoB f) implies LSeg ((((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|),(((1 / 2) * (((GoB f) * ((i + 1),(width (GoB f)))) + ((GoB f) * ((i + 2),(width (GoB f)))))) + |[0,1]|)) misses L~ f )
assume that
A1: 1 <= i and
A2: i + 2 <= len (GoB f) ; ::_thesis: LSeg ((((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|),(((1 / 2) * (((GoB f) * ((i + 1),(width (GoB f)))) + ((GoB f) * ((i + 2),(width (GoB f)))))) + |[0,1]|)) misses L~ f
A3: 1 <= width (GoB f) by GOBOARD7:33;
now__::_thesis:_for_p_being_Point_of_(TOP-REAL_2)_st_p_in_LSeg_((((1_/_2)_*_(((GoB_f)_*_(i,(width_(GoB_f))))_+_((GoB_f)_*_((i_+_1),(width_(GoB_f))))))_+_|[0,1]|),(((1_/_2)_*_(((GoB_f)_*_((i_+_1),(width_(GoB_f))))_+_((GoB_f)_*_((i_+_2),(width_(GoB_f))))))_+_|[0,1]|))_holds_
p_`2_>_((GoB_f)_*_(1,(width_(GoB_f))))_`2
A4: i <= i + 2 by NAT_1:11;
then  i <= len (GoB f) by A2, XXREAL_0:2;
then A5: ((GoB f) * (i,(width (GoB f)))) `2 = ((GoB f) * (1,(width (GoB f)))) `2 by A1, A3, GOBOARD5:1;
 i + 1 <= i + 2 by XREAL_1:6;
then  ( 1 <= i + 1 & i + 1 <= len (GoB f) ) by A2, NAT_1:11, XXREAL_0:2;
then A6: ((GoB f) * ((i + 1),(width (GoB f)))) `2 = ((GoB f) * (1,(width (GoB f)))) `2 by A3, GOBOARD5:1;
 1 <= i + 2 by A1, A4, XXREAL_0:2;
then A7: ((GoB f) * ((i + 2),(width (GoB f)))) `2 = ((GoB f) * (1,(width (GoB f)))) `2 by A2, A3, GOBOARD5:1;
(((1 / 2) * (((GoB f) * ((i + 1),(width (GoB f)))) + ((GoB f) * ((i + 2),(width (GoB f)))))) + |[0,1]|) `2 = (((1 / 2) * (((GoB f) * ((i + 1),(width (GoB f)))) + ((GoB f) * ((i + 2),(width (GoB f)))))) `2) + (|[0,1]| `2) by TOPREAL3:2
.= ((1 / 2) * ((((GoB f) * ((i + 1),(width (GoB f)))) + ((GoB f) * ((i + 2),(width (GoB f))))) `2)) + (|[0,1]| `2) by TOPREAL3:4
.= ((1 / 2) * ((((GoB f) * (1,(width (GoB f)))) `2) + (((GoB f) * (1,(width (GoB f)))) `2))) + (|[0,1]| `2) by A6, A7, TOPREAL3:2
.= (1 * (((GoB f) * (1,(width (GoB f)))) `2)) + 1 by EUCLID:52 ;
then A8: ((1 / 2) * (((GoB f) * ((i + 1),(width (GoB f)))) + ((GoB f) * ((i + 2),(width (GoB f)))))) + |[0,1]| = |[((((1 / 2) * (((GoB f) * ((i + 1),(width (GoB f)))) + ((GoB f) * ((i + 2),(width (GoB f)))))) + |[0,1]|) `1),((((GoB f) * (1,(width (GoB f)))) `2) + 1)]| by EUCLID:53;
(((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|) `2 = (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `2) + (|[0,1]| `2) by TOPREAL3:2
.= ((1 / 2) * ((((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) `2)) + (|[0,1]| `2) by TOPREAL3:4
.= ((1 / 2) * ((((GoB f) * (1,(width (GoB f)))) `2) + (((GoB f) * (1,(width (GoB f)))) `2))) + (|[0,1]| `2) by A5, A6, TOPREAL3:2
.= (1 * (((GoB f) * (1,(width (GoB f)))) `2)) + 1 by EUCLID:52 ;
then A9: ((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]| = |[((((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|) `1),((((GoB f) * (1,(width (GoB f)))) `2) + 1)]| by EUCLID:53;
let p be Point of (TOP-REAL 2); ::_thesis: ( p in LSeg ((((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|),(((1 / 2) * (((GoB f) * ((i + 1),(width (GoB f)))) + ((GoB f) * ((i + 2),(width (GoB f)))))) + |[0,1]|)) implies p `2 > ((GoB f) * (1,(width (GoB f)))) `2 )
assume  p in LSeg ((((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|),(((1 / 2) * (((GoB f) * ((i + 1),(width (GoB f)))) + ((GoB f) * ((i + 2),(width (GoB f)))))) + |[0,1]|)) ; ::_thesis: p `2 > ((GoB f) * (1,(width (GoB f)))) `2
then  p `2 = (((GoB f) * (1,(width (GoB f)))) `2) + 1 by A9, A8, TOPREAL3:12;
hence  p `2 > ((GoB f) * (1,(width (GoB f)))) `2 by XREAL_1:29; ::_thesis: verum
end;
hence  LSeg ((((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|),(((1 / 2) * (((GoB f) * ((i + 1),(width (GoB f)))) + ((GoB f) * ((i + 2),(width (GoB f)))))) + |[0,1]|)) misses L~ f by Th24; ::_thesis: verum
end;

theorem :: GOBOARD8:29
for f being non constant standard special_circular_sequence holds LSeg ((((GoB f) * (1,(width (GoB f)))) + |[(- 1),1]|),(((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * (2,(width (GoB f)))))) + |[0,1]|)) misses L~ f
proof
let f be non constant standard special_circular_sequence; ::_thesis: LSeg ((((GoB f) * (1,(width (GoB f)))) + |[(- 1),1]|),(((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * (2,(width (GoB f)))))) + |[0,1]|)) misses L~ f
A1: 1 <= width (GoB f) by GOBOARD7:33;
now__::_thesis:_for_p_being_Point_of_(TOP-REAL_2)_st_p_in_LSeg_((((GoB_f)_*_(1,(width_(GoB_f))))_+_|[(-_1),1]|),(((1_/_2)_*_(((GoB_f)_*_(1,(width_(GoB_f))))_+_((GoB_f)_*_(2,(width_(GoB_f))))))_+_|[0,1]|))_holds_
p_`2_>_((GoB_f)_*_(1,(width_(GoB_f))))_`2
 1 < len (GoB f) by GOBOARD7:32;
then  1 + 1 <= len (GoB f) by NAT_1:13;
then A2: ((GoB f) * (2,(width (GoB f)))) `2 = ((GoB f) * (1,(width (GoB f)))) `2 by A1, GOBOARD5:1;
(((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * (2,(width (GoB f)))))) + |[0,1]|) `2 = (((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * (2,(width (GoB f)))))) `2) + (|[0,1]| `2) by TOPREAL3:2
.= ((1 / 2) * ((((GoB f) * (1,(width (GoB f)))) + ((GoB f) * (2,(width (GoB f))))) `2)) + (|[0,1]| `2) by TOPREAL3:4
.= ((1 / 2) * ((((GoB f) * (1,(width (GoB f)))) `2) + (((GoB f) * (1,(width (GoB f)))) `2))) + (|[0,1]| `2) by A2, TOPREAL3:2
.= (1 * (((GoB f) * (1,(width (GoB f)))) `2)) + 1 by EUCLID:52 ;
then A3: ((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * (2,(width (GoB f)))))) + |[0,1]| = |[((((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * (2,(width (GoB f)))))) + |[0,1]|) `1),((((GoB f) * (1,(width (GoB f)))) `2) + 1)]| by EUCLID:53;
(((GoB f) * (1,(width (GoB f)))) + |[(- 1),1]|) `2 = (((GoB f) * (1,(width (GoB f)))) `2) + (|[(- 1),1]| `2) by TOPREAL3:2
.= (((GoB f) * (1,(width (GoB f)))) `2) + 1 by EUCLID:52 ;
then A4: ((GoB f) * (1,(width (GoB f)))) + |[(- 1),1]| = |[((((GoB f) * (1,(width (GoB f)))) + |[(- 1),1]|) `1),((((GoB f) * (1,(width (GoB f)))) `2) + 1)]| by EUCLID:53;
let p be Point of (TOP-REAL 2); ::_thesis: ( p in LSeg ((((GoB f) * (1,(width (GoB f)))) + |[(- 1),1]|),(((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * (2,(width (GoB f)))))) + |[0,1]|)) implies p `2 > ((GoB f) * (1,(width (GoB f)))) `2 )
assume  p in LSeg ((((GoB f) * (1,(width (GoB f)))) + |[(- 1),1]|),(((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * (2,(width (GoB f)))))) + |[0,1]|)) ; ::_thesis: p `2 > ((GoB f) * (1,(width (GoB f)))) `2
then  p `2 = (((GoB f) * (1,(width (GoB f)))) `2) + 1 by A4, A3, TOPREAL3:12;
hence  p `2 > ((GoB f) * (1,(width (GoB f)))) `2 by XREAL_1:29; ::_thesis: verum
end;
hence  LSeg ((((GoB f) * (1,(width (GoB f)))) + |[(- 1),1]|),(((1 / 2) * (((GoB f) * (1,(width (GoB f)))) + ((GoB f) * (2,(width (GoB f)))))) + |[0,1]|)) misses L~ f by Th24; ::_thesis: verum
end;

theorem :: GOBOARD8:30
for f being non constant standard special_circular_sequence holds LSeg ((((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),(width (GoB f)))) + ((GoB f) * ((len (GoB f)),(width (GoB f)))))) + |[0,1]|),(((GoB f) * ((len (GoB f)),(width (GoB f)))) + |[1,1]|)) misses L~ f
proof
let f be non constant standard special_circular_sequence; ::_thesis: LSeg ((((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),(width (GoB f)))) + ((GoB f) * ((len (GoB f)),(width (GoB f)))))) + |[0,1]|),(((GoB f) * ((len (GoB f)),(width (GoB f)))) + |[1,1]|)) misses L~ f
A1: 1 <= width (GoB f) by GOBOARD7:33;
now__::_thesis:_for_p_being_Point_of_(TOP-REAL_2)_st_p_in_LSeg_((((1_/_2)_*_(((GoB_f)_*_(((len_(GoB_f))_-'_1),(width_(GoB_f))))_+_((GoB_f)_*_((len_(GoB_f)),(width_(GoB_f))))))_+_|[0,1]|),(((GoB_f)_*_((len_(GoB_f)),(width_(GoB_f))))_+_|[1,1]|))_holds_
p_`2_>_((GoB_f)_*_(1,(width_(GoB_f))))_`2
A2: 1 < len (GoB f) by GOBOARD7:32;
then A3: ((len (GoB f)) -' 1) + 1 = len (GoB f) by XREAL_1:235;
then A4: (len (GoB f)) -' 1 <= len (GoB f) by NAT_1:11;
A5: ((GoB f) * ((len (GoB f)),(width (GoB f)))) `2 = ((GoB f) * (1,(width (GoB f)))) `2 by A1, A2, GOBOARD5:1;
then (((GoB f) * ((len (GoB f)),(width (GoB f)))) + |[1,1]|) `2 = (((GoB f) * (1,(width (GoB f)))) `2) + (|[1,1]| `2) by TOPREAL3:2
.= (((GoB f) * (1,(width (GoB f)))) `2) + 1 by EUCLID:52 ;
then A6: ((GoB f) * ((len (GoB f)),(width (GoB f)))) + |[1,1]| = |[((((GoB f) * ((len (GoB f)),(width (GoB f)))) + |[1,1]|) `1),((((GoB f) * (1,(width (GoB f)))) `2) + 1)]| by EUCLID:53;
 1 <= (len (GoB f)) -' 1 by A2, A3, NAT_1:13;
then A7: ((GoB f) * (((len (GoB f)) -' 1),(width (GoB f)))) `2 = ((GoB f) * (1,(width (GoB f)))) `2 by A1, A4, GOBOARD5:1;
(((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),(width (GoB f)))) + ((GoB f) * ((len (GoB f)),(width (GoB f)))))) + |[0,1]|) `2 = (((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),(width (GoB f)))) + ((GoB f) * ((len (GoB f)),(width (GoB f)))))) `2) + (|[0,1]| `2) by TOPREAL3:2
.= ((1 / 2) * ((((GoB f) * (((len (GoB f)) -' 1),(width (GoB f)))) + ((GoB f) * ((len (GoB f)),(width (GoB f))))) `2)) + (|[0,1]| `2) by TOPREAL3:4
.= ((1 / 2) * ((((GoB f) * (1,(width (GoB f)))) `2) + (((GoB f) * (1,(width (GoB f)))) `2))) + (|[0,1]| `2) by A7, A5, TOPREAL3:2
.= (1 * (((GoB f) * (1,(width (GoB f)))) `2)) + 1 by EUCLID:52 ;
then A8: ((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),(width (GoB f)))) + ((GoB f) * ((len (GoB f)),(width (GoB f)))))) + |[0,1]| = |[((((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),(width (GoB f)))) + ((GoB f) * ((len (GoB f)),(width (GoB f)))))) + |[0,1]|) `1),((((GoB f) * (1,(width (GoB f)))) `2) + 1)]| by EUCLID:53;
let p be Point of (TOP-REAL 2); ::_thesis: ( p in LSeg ((((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),(width (GoB f)))) + ((GoB f) * ((len (GoB f)),(width (GoB f)))))) + |[0,1]|),(((GoB f) * ((len (GoB f)),(width (GoB f)))) + |[1,1]|)) implies p `2 > ((GoB f) * (1,(width (GoB f)))) `2 )
assume  p in LSeg ((((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),(width (GoB f)))) + ((GoB f) * ((len (GoB f)),(width (GoB f)))))) + |[0,1]|),(((GoB f) * ((len (GoB f)),(width (GoB f)))) + |[1,1]|)) ; ::_thesis: p `2 > ((GoB f) * (1,(width (GoB f)))) `2
then  p `2 = (((GoB f) * (1,(width (GoB f)))) `2) + 1 by A8, A6, TOPREAL3:12;
hence  p `2 > ((GoB f) * (1,(width (GoB f)))) `2 by XREAL_1:29; ::_thesis: verum
end;
hence  LSeg ((((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),(width (GoB f)))) + ((GoB f) * ((len (GoB f)),(width (GoB f)))))) + |[0,1]|),(((GoB f) * ((len (GoB f)),(width (GoB f)))) + |[1,1]|)) misses L~ f by Th24; ::_thesis: verum
end;

theorem :: GOBOARD8:31
for f being non constant standard special_circular_sequence
for j being Element of NAT st 1 <= j & j + 2 <= width (GoB f) holds
LSeg ((((1 / 2) * (((GoB f) * (1,j)) + ((GoB f) * (1,(j + 1))))) - |[1,0]|),(((1 / 2) * (((GoB f) * (1,(j + 1))) + ((GoB f) * (1,(j + 2))))) - |[1,0]|)) misses L~ f
proof
let f be non constant standard special_circular_sequence; ::_thesis: for j being Element of NAT st 1 <= j & j + 2 <= width (GoB f) holds
LSeg ((((1 / 2) * (((GoB f) * (1,j)) + ((GoB f) * (1,(j + 1))))) - |[1,0]|),(((1 / 2) * (((GoB f) * (1,(j + 1))) + ((GoB f) * (1,(j + 2))))) - |[1,0]|)) misses L~ f
let j be Element of NAT ; ::_thesis: ( 1 <= j & j + 2 <= width (GoB f) implies LSeg ((((1 / 2) * (((GoB f) * (1,j)) + ((GoB f) * (1,(j + 1))))) - |[1,0]|),(((1 / 2) * (((GoB f) * (1,(j + 1))) + ((GoB f) * (1,(j + 2))))) - |[1,0]|)) misses L~ f )
assume that
A1: 1 <= j and
A2: j + 2 <= width (GoB f) ; ::_thesis: LSeg ((((1 / 2) * (((GoB f) * (1,j)) + ((GoB f) * (1,(j + 1))))) - |[1,0]|),(((1 / 2) * (((GoB f) * (1,(j + 1))) + ((GoB f) * (1,(j + 2))))) - |[1,0]|)) misses L~ f
A3: 1 <= len (GoB f) by GOBOARD7:32;
now__::_thesis:_for_p_being_Point_of_(TOP-REAL_2)_st_p_in_LSeg_((((1_/_2)_*_(((GoB_f)_*_(1,j))_+_((GoB_f)_*_(1,(j_+_1)))))_-_|[1,0]|),(((1_/_2)_*_(((GoB_f)_*_(1,(j_+_1)))_+_((GoB_f)_*_(1,(j_+_2)))))_-_|[1,0]|))_holds_
p_`1_<_((GoB_f)_*_(1,1))_`1
A4: j <= j + 2 by NAT_1:11;
then  j <= width (GoB f) by A2, XXREAL_0:2;
then A5: ((GoB f) * (1,j)) `1 = ((GoB f) * (1,1)) `1 by A1, A3, GOBOARD5:2;
 j + 1 <= j + 2 by XREAL_1:6;
then  ( 1 <= j + 1 & j + 1 <= width (GoB f) ) by A2, NAT_1:11, XXREAL_0:2;
then A6: ((GoB f) * (1,(j + 1))) `1 = ((GoB f) * (1,1)) `1 by A3, GOBOARD5:2;
 1 <= j + 2 by A1, A4, XXREAL_0:2;
then A7: ((GoB f) * (1,(j + 2))) `1 = ((GoB f) * (1,1)) `1 by A2, A3, GOBOARD5:2;
(((1 / 2) * (((GoB f) * (1,(j + 1))) + ((GoB f) * (1,(j + 2))))) - |[1,0]|) `1 = (((1 / 2) * (((GoB f) * (1,(j + 1))) + ((GoB f) * (1,(j + 2))))) `1) - (|[1,0]| `1) by TOPREAL3:3
.= ((1 / 2) * ((((GoB f) * (1,(j + 1))) + ((GoB f) * (1,(j + 2)))) `1)) - (|[1,0]| `1) by TOPREAL3:4
.= ((1 / 2) * ((((GoB f) * (1,1)) `1) + (((GoB f) * (1,1)) `1))) - (|[1,0]| `1) by A6, A7, TOPREAL3:2
.= (1 * (((GoB f) * (1,1)) `1)) - 1 by EUCLID:52 ;
then A8: ((1 / 2) * (((GoB f) * (1,(j + 1))) + ((GoB f) * (1,(j + 2))))) - |[1,0]| = |[((((GoB f) * (1,1)) `1) - 1),((((1 / 2) * (((GoB f) * (1,(j + 1))) + ((GoB f) * (1,(j + 2))))) - |[1,0]|) `2)]| by EUCLID:53;
(((1 / 2) * (((GoB f) * (1,j)) + ((GoB f) * (1,(j + 1))))) - |[1,0]|) `1 = (((1 / 2) * (((GoB f) * (1,j)) + ((GoB f) * (1,(j + 1))))) `1) - (|[1,0]| `1) by TOPREAL3:3
.= ((1 / 2) * ((((GoB f) * (1,j)) + ((GoB f) * (1,(j + 1)))) `1)) - (|[1,0]| `1) by TOPREAL3:4
.= ((1 / 2) * ((((GoB f) * (1,1)) `1) + (((GoB f) * (1,1)) `1))) - (|[1,0]| `1) by A5, A6, TOPREAL3:2
.= (1 * (((GoB f) * (1,1)) `1)) - 1 by EUCLID:52 ;
then A9: ((1 / 2) * (((GoB f) * (1,j)) + ((GoB f) * (1,(j + 1))))) - |[1,0]| = |[((((GoB f) * (1,1)) `1) - 1),((((1 / 2) * (((GoB f) * (1,j)) + ((GoB f) * (1,(j + 1))))) - |[1,0]|) `2)]| by EUCLID:53;
let p be Point of (TOP-REAL 2); ::_thesis: ( p in LSeg ((((1 / 2) * (((GoB f) * (1,j)) + ((GoB f) * (1,(j + 1))))) - |[1,0]|),(((1 / 2) * (((GoB f) * (1,(j + 1))) + ((GoB f) * (1,(j + 2))))) - |[1,0]|)) implies p `1 < ((GoB f) * (1,1)) `1 )
assume  p in LSeg ((((1 / 2) * (((GoB f) * (1,j)) + ((GoB f) * (1,(j + 1))))) - |[1,0]|),(((1 / 2) * (((GoB f) * (1,(j + 1))) + ((GoB f) * (1,(j + 2))))) - |[1,0]|)) ; ::_thesis: p `1 < ((GoB f) * (1,1)) `1
then  p `1 = (((GoB f) * (1,1)) `1) - 1 by A9, A8, TOPREAL3:11;
hence  p `1 < ((GoB f) * (1,1)) `1 by XREAL_1:44; ::_thesis: verum
end;
hence  LSeg ((((1 / 2) * (((GoB f) * (1,j)) + ((GoB f) * (1,(j + 1))))) - |[1,0]|),(((1 / 2) * (((GoB f) * (1,(j + 1))) + ((GoB f) * (1,(j + 2))))) - |[1,0]|)) misses L~ f by Th21; ::_thesis: verum
end;

theorem :: GOBOARD8:32
for f being non constant standard special_circular_sequence holds LSeg ((((GoB f) * (1,1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (1,2)))) - |[1,0]|)) misses L~ f
proof
let f be non constant standard special_circular_sequence; ::_thesis: LSeg ((((GoB f) * (1,1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (1,2)))) - |[1,0]|)) misses L~ f
A1: 1 <= len (GoB f) by GOBOARD7:32;
now__::_thesis:_for_p_being_Point_of_(TOP-REAL_2)_st_p_in_LSeg_((((GoB_f)_*_(1,1))_-_|[1,1]|),(((1_/_2)_*_(((GoB_f)_*_(1,1))_+_((GoB_f)_*_(1,2))))_-_|[1,0]|))_holds_
p_`1_<_((GoB_f)_*_(1,1))_`1
 1 < width (GoB f) by GOBOARD7:33;
then  1 + 1 <= width (GoB f) by NAT_1:13;
then A2: ((GoB f) * (1,2)) `1 = ((GoB f) * (1,1)) `1 by A1, GOBOARD5:2;
(((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (1,2)))) - |[1,0]|) `1 = (((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (1,2)))) `1) - (|[1,0]| `1) by TOPREAL3:3
.= ((1 / 2) * ((((GoB f) * (1,1)) + ((GoB f) * (1,2))) `1)) - (|[1,0]| `1) by TOPREAL3:4
.= ((1 / 2) * ((((GoB f) * (1,1)) `1) + (((GoB f) * (1,1)) `1))) - (|[1,0]| `1) by A2, TOPREAL3:2
.= (1 * (((GoB f) * (1,1)) `1)) - 1 by EUCLID:52 ;
then A3: ((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (1,2)))) - |[1,0]| = |[((((GoB f) * (1,1)) `1) - 1),((((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (1,2)))) - |[1,0]|) `2)]| by EUCLID:53;
(((GoB f) * (1,1)) - |[1,1]|) `1 = (((GoB f) * (1,1)) `1) - (|[1,1]| `1) by TOPREAL3:3
.= (((GoB f) * (1,1)) `1) - 1 by EUCLID:52 ;
then A4: ((GoB f) * (1,1)) - |[1,1]| = |[((((GoB f) * (1,1)) `1) - 1),((((GoB f) * (1,1)) - |[1,1]|) `2)]| by EUCLID:53;
let p be Point of (TOP-REAL 2); ::_thesis: ( p in LSeg ((((GoB f) * (1,1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (1,2)))) - |[1,0]|)) implies p `1 < ((GoB f) * (1,1)) `1 )
assume  p in LSeg ((((GoB f) * (1,1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (1,2)))) - |[1,0]|)) ; ::_thesis: p `1 < ((GoB f) * (1,1)) `1
then  p `1 = (((GoB f) * (1,1)) `1) - 1 by A4, A3, TOPREAL3:11;
hence  p `1 < ((GoB f) * (1,1)) `1 by XREAL_1:44; ::_thesis: verum
end;
hence  LSeg ((((GoB f) * (1,1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (1,1)) + ((GoB f) * (1,2)))) - |[1,0]|)) misses L~ f by Th21; ::_thesis: verum
end;

theorem :: GOBOARD8:33
for f being non constant standard special_circular_sequence holds LSeg ((((1 / 2) * (((GoB f) * (1,((width (GoB f)) -' 1))) + ((GoB f) * (1,(width (GoB f)))))) - |[1,0]|),(((GoB f) * (1,(width (GoB f)))) + |[(- 1),1]|)) misses L~ f
proof
let f be non constant standard special_circular_sequence; ::_thesis: LSeg ((((1 / 2) * (((GoB f) * (1,((width (GoB f)) -' 1))) + ((GoB f) * (1,(width (GoB f)))))) - |[1,0]|),(((GoB f) * (1,(width (GoB f)))) + |[(- 1),1]|)) misses L~ f
A1: 1 <= len (GoB f) by GOBOARD7:32;
now__::_thesis:_for_p_being_Point_of_(TOP-REAL_2)_st_p_in_LSeg_((((1_/_2)_*_(((GoB_f)_*_(1,((width_(GoB_f))_-'_1)))_+_((GoB_f)_*_(1,(width_(GoB_f))))))_-_|[1,0]|),(((GoB_f)_*_(1,(width_(GoB_f))))_+_|[(-_1),1]|))_holds_
p_`1_<_((GoB_f)_*_(1,1))_`1
A2: 1 < width (GoB f) by GOBOARD7:33;
then A3: ((width (GoB f)) -' 1) + 1 = width (GoB f) by XREAL_1:235;
then A4: (width (GoB f)) -' 1 <= width (GoB f) by NAT_1:11;
A5: ((GoB f) * (1,(width (GoB f)))) `1 = ((GoB f) * (1,1)) `1 by A1, A2, GOBOARD5:2;
then (((GoB f) * (1,(width (GoB f)))) + |[(- 1),1]|) `1 = (((GoB f) * (1,1)) `1) + (|[(- 1),1]| `1) by TOPREAL3:2
.= (((GoB f) * (1,1)) `1) + (- 1) by EUCLID:52
.= (((GoB f) * (1,1)) `1) - 1 ;
then A6: ((GoB f) * (1,(width (GoB f)))) + |[(- 1),1]| = |[((((GoB f) * (1,1)) `1) - 1),((((GoB f) * (1,(width (GoB f)))) + |[(- 1),1]|) `2)]| by EUCLID:53;
 1 <= (width (GoB f)) -' 1 by A2, A3, NAT_1:13;
then A7: ((GoB f) * (1,((width (GoB f)) -' 1))) `1 = ((GoB f) * (1,1)) `1 by A1, A4, GOBOARD5:2;
(((1 / 2) * (((GoB f) * (1,((width (GoB f)) -' 1))) + ((GoB f) * (1,(width (GoB f)))))) - |[1,0]|) `1 = (((1 / 2) * (((GoB f) * (1,((width (GoB f)) -' 1))) + ((GoB f) * (1,(width (GoB f)))))) `1) - (|[1,0]| `1) by TOPREAL3:3
.= ((1 / 2) * ((((GoB f) * (1,((width (GoB f)) -' 1))) + ((GoB f) * (1,(width (GoB f))))) `1)) - (|[1,0]| `1) by TOPREAL3:4
.= ((1 / 2) * ((((GoB f) * (1,1)) `1) + (((GoB f) * (1,1)) `1))) - (|[1,0]| `1) by A7, A5, TOPREAL3:2
.= (1 * (((GoB f) * (1,1)) `1)) - 1 by EUCLID:52 ;
then A8: ((1 / 2) * (((GoB f) * (1,((width (GoB f)) -' 1))) + ((GoB f) * (1,(width (GoB f)))))) - |[1,0]| = |[((((GoB f) * (1,1)) `1) - 1),((((1 / 2) * (((GoB f) * (1,((width (GoB f)) -' 1))) + ((GoB f) * (1,(width (GoB f)))))) - |[1,0]|) `2)]| by EUCLID:53;
let p be Point of (TOP-REAL 2); ::_thesis: ( p in LSeg ((((1 / 2) * (((GoB f) * (1,((width (GoB f)) -' 1))) + ((GoB f) * (1,(width (GoB f)))))) - |[1,0]|),(((GoB f) * (1,(width (GoB f)))) + |[(- 1),1]|)) implies p `1 < ((GoB f) * (1,1)) `1 )
assume  p in LSeg ((((1 / 2) * (((GoB f) * (1,((width (GoB f)) -' 1))) + ((GoB f) * (1,(width (GoB f)))))) - |[1,0]|),(((GoB f) * (1,(width (GoB f)))) + |[(- 1),1]|)) ; ::_thesis: p `1 < ((GoB f) * (1,1)) `1
then  p `1 = (((GoB f) * (1,1)) `1) - 1 by A8, A6, TOPREAL3:11;
hence  p `1 < ((GoB f) * (1,1)) `1 by XREAL_1:44; ::_thesis: verum
end;
hence  LSeg ((((1 / 2) * (((GoB f) * (1,((width (GoB f)) -' 1))) + ((GoB f) * (1,(width (GoB f)))))) - |[1,0]|),(((GoB f) * (1,(width (GoB f)))) + |[(- 1),1]|)) misses L~ f by Th21; ::_thesis: verum
end;

theorem :: GOBOARD8:34
for f being non constant standard special_circular_sequence
for j being Element of NAT st 1 <= j & j + 2 <= width (GoB f) holds
LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),j)) + ((GoB f) * ((len (GoB f)),(j + 1))))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),(j + 1))) + ((GoB f) * ((len (GoB f)),(j + 2))))) + |[1,0]|)) misses L~ f
proof
let f be non constant standard special_circular_sequence; ::_thesis: for j being Element of NAT st 1 <= j & j + 2 <= width (GoB f) holds
LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),j)) + ((GoB f) * ((len (GoB f)),(j + 1))))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),(j + 1))) + ((GoB f) * ((len (GoB f)),(j + 2))))) + |[1,0]|)) misses L~ f
let j be Element of NAT ; ::_thesis: ( 1 <= j & j + 2 <= width (GoB f) implies LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),j)) + ((GoB f) * ((len (GoB f)),(j + 1))))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),(j + 1))) + ((GoB f) * ((len (GoB f)),(j + 2))))) + |[1,0]|)) misses L~ f )
assume that
A1: 1 <= j and
A2: j + 2 <= width (GoB f) ; ::_thesis: LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),j)) + ((GoB f) * ((len (GoB f)),(j + 1))))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),(j + 1))) + ((GoB f) * ((len (GoB f)),(j + 2))))) + |[1,0]|)) misses L~ f
A3: 1 <= len (GoB f) by GOBOARD7:32;
now__::_thesis:_for_p_being_Point_of_(TOP-REAL_2)_st_p_in_LSeg_((((1_/_2)_*_(((GoB_f)_*_((len_(GoB_f)),j))_+_((GoB_f)_*_((len_(GoB_f)),(j_+_1)))))_+_|[1,0]|),(((1_/_2)_*_(((GoB_f)_*_((len_(GoB_f)),(j_+_1)))_+_((GoB_f)_*_((len_(GoB_f)),(j_+_2)))))_+_|[1,0]|))_holds_
p_`1_>_((GoB_f)_*_((len_(GoB_f)),1))_`1
A4: j <= j + 2 by NAT_1:11;
then  j <= width (GoB f) by A2, XXREAL_0:2;
then A5: ((GoB f) * ((len (GoB f)),j)) `1 = ((GoB f) * ((len (GoB f)),1)) `1 by A1, A3, GOBOARD5:2;
 j + 1 <= j + 2 by XREAL_1:6;
then  ( 1 <= j + 1 & j + 1 <= width (GoB f) ) by A2, NAT_1:11, XXREAL_0:2;
then A6: ((GoB f) * ((len (GoB f)),(j + 1))) `1 = ((GoB f) * ((len (GoB f)),1)) `1 by A3, GOBOARD5:2;
 1 <= j + 2 by A1, A4, XXREAL_0:2;
then A7: ((GoB f) * ((len (GoB f)),(j + 2))) `1 = ((GoB f) * ((len (GoB f)),1)) `1 by A2, A3, GOBOARD5:2;
(((1 / 2) * (((GoB f) * ((len (GoB f)),(j + 1))) + ((GoB f) * ((len (GoB f)),(j + 2))))) + |[1,0]|) `1 = (((1 / 2) * (((GoB f) * ((len (GoB f)),(j + 1))) + ((GoB f) * ((len (GoB f)),(j + 2))))) `1) + (|[1,0]| `1) by TOPREAL3:2
.= ((1 / 2) * ((((GoB f) * ((len (GoB f)),(j + 1))) + ((GoB f) * ((len (GoB f)),(j + 2)))) `1)) + (|[1,0]| `1) by TOPREAL3:4
.= ((1 / 2) * ((((GoB f) * ((len (GoB f)),1)) `1) + (((GoB f) * ((len (GoB f)),1)) `1))) + (|[1,0]| `1) by A6, A7, TOPREAL3:2
.= (1 * (((GoB f) * ((len (GoB f)),1)) `1)) + 1 by EUCLID:52 ;
then A8: ((1 / 2) * (((GoB f) * ((len (GoB f)),(j + 1))) + ((GoB f) * ((len (GoB f)),(j + 2))))) + |[1,0]| = |[((((GoB f) * ((len (GoB f)),1)) `1) + 1),((((1 / 2) * (((GoB f) * ((len (GoB f)),(j + 1))) + ((GoB f) * ((len (GoB f)),(j + 2))))) + |[1,0]|) `2)]| by EUCLID:53;
(((1 / 2) * (((GoB f) * ((len (GoB f)),j)) + ((GoB f) * ((len (GoB f)),(j + 1))))) + |[1,0]|) `1 = (((1 / 2) * (((GoB f) * ((len (GoB f)),j)) + ((GoB f) * ((len (GoB f)),(j + 1))))) `1) + (|[1,0]| `1) by TOPREAL3:2
.= ((1 / 2) * ((((GoB f) * ((len (GoB f)),j)) + ((GoB f) * ((len (GoB f)),(j + 1)))) `1)) + (|[1,0]| `1) by TOPREAL3:4
.= ((1 / 2) * ((((GoB f) * ((len (GoB f)),1)) `1) + (((GoB f) * ((len (GoB f)),1)) `1))) + (|[1,0]| `1) by A5, A6, TOPREAL3:2
.= (1 * (((GoB f) * ((len (GoB f)),1)) `1)) + 1 by EUCLID:52 ;
then A9: ((1 / 2) * (((GoB f) * ((len (GoB f)),j)) + ((GoB f) * ((len (GoB f)),(j + 1))))) + |[1,0]| = |[((((GoB f) * ((len (GoB f)),1)) `1) + 1),((((1 / 2) * (((GoB f) * ((len (GoB f)),j)) + ((GoB f) * ((len (GoB f)),(j + 1))))) + |[1,0]|) `2)]| by EUCLID:53;
let p be Point of (TOP-REAL 2); ::_thesis: ( p in LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),j)) + ((GoB f) * ((len (GoB f)),(j + 1))))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),(j + 1))) + ((GoB f) * ((len (GoB f)),(j + 2))))) + |[1,0]|)) implies p `1 > ((GoB f) * ((len (GoB f)),1)) `1 )
assume  p in LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),j)) + ((GoB f) * ((len (GoB f)),(j + 1))))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),(j + 1))) + ((GoB f) * ((len (GoB f)),(j + 2))))) + |[1,0]|)) ; ::_thesis: p `1 > ((GoB f) * ((len (GoB f)),1)) `1
then  p `1 = (((GoB f) * ((len (GoB f)),1)) `1) + 1 by A9, A8, TOPREAL3:11;
hence  p `1 > ((GoB f) * ((len (GoB f)),1)) `1 by XREAL_1:29; ::_thesis: verum
end;
hence  LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),j)) + ((GoB f) * ((len (GoB f)),(j + 1))))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),(j + 1))) + ((GoB f) * ((len (GoB f)),(j + 2))))) + |[1,0]|)) misses L~ f by Th22; ::_thesis: verum
end;

theorem :: GOBOARD8:35
for f being non constant standard special_circular_sequence holds LSeg ((((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),1)) + ((GoB f) * ((len (GoB f)),2)))) + |[1,0]|)) misses L~ f
proof
let f be non constant standard special_circular_sequence; ::_thesis: LSeg ((((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),1)) + ((GoB f) * ((len (GoB f)),2)))) + |[1,0]|)) misses L~ f
A1: 1 <= len (GoB f) by GOBOARD7:32;
now__::_thesis:_for_p_being_Point_of_(TOP-REAL_2)_st_p_in_LSeg_((((GoB_f)_*_((len_(GoB_f)),1))_+_|[1,(-_1)]|),(((1_/_2)_*_(((GoB_f)_*_((len_(GoB_f)),1))_+_((GoB_f)_*_((len_(GoB_f)),2))))_+_|[1,0]|))_holds_
p_`1_>_((GoB_f)_*_((len_(GoB_f)),1))_`1
 1 < width (GoB f) by GOBOARD7:33;
then  1 + 1 <= width (GoB f) by NAT_1:13;
then A2: ((GoB f) * ((len (GoB f)),2)) `1 = ((GoB f) * ((len (GoB f)),1)) `1 by A1, GOBOARD5:2;
(((1 / 2) * (((GoB f) * ((len (GoB f)),1)) + ((GoB f) * ((len (GoB f)),2)))) + |[1,0]|) `1 = (((1 / 2) * (((GoB f) * ((len (GoB f)),1)) + ((GoB f) * ((len (GoB f)),2)))) `1) + (|[1,0]| `1) by TOPREAL3:2
.= ((1 / 2) * ((((GoB f) * ((len (GoB f)),1)) + ((GoB f) * ((len (GoB f)),2))) `1)) + (|[1,0]| `1) by TOPREAL3:4
.= ((1 / 2) * ((((GoB f) * ((len (GoB f)),1)) `1) + (((GoB f) * ((len (GoB f)),1)) `1))) + (|[1,0]| `1) by A2, TOPREAL3:2
.= (1 * (((GoB f) * ((len (GoB f)),1)) `1)) + 1 by EUCLID:52 ;
then A3: ((1 / 2) * (((GoB f) * ((len (GoB f)),1)) + ((GoB f) * ((len (GoB f)),2)))) + |[1,0]| = |[((((GoB f) * ((len (GoB f)),1)) `1) + 1),((((1 / 2) * (((GoB f) * ((len (GoB f)),1)) + ((GoB f) * ((len (GoB f)),2)))) + |[1,0]|) `2)]| by EUCLID:53;
(((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|) `1 = (((GoB f) * ((len (GoB f)),1)) `1) + (|[1,(- 1)]| `1) by TOPREAL3:2
.= (((GoB f) * ((len (GoB f)),1)) `1) + 1 by EUCLID:52 ;
then A4: ((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]| = |[((((GoB f) * ((len (GoB f)),1)) `1) + 1),((((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|) `2)]| by EUCLID:53;
let p be Point of (TOP-REAL 2); ::_thesis: ( p in LSeg ((((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),1)) + ((GoB f) * ((len (GoB f)),2)))) + |[1,0]|)) implies p `1 > ((GoB f) * ((len (GoB f)),1)) `1 )
assume  p in LSeg ((((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),1)) + ((GoB f) * ((len (GoB f)),2)))) + |[1,0]|)) ; ::_thesis: p `1 > ((GoB f) * ((len (GoB f)),1)) `1
then  p `1 = (((GoB f) * ((len (GoB f)),1)) `1) + 1 by A4, A3, TOPREAL3:11;
hence  p `1 > ((GoB f) * ((len (GoB f)),1)) `1 by XREAL_1:29; ::_thesis: verum
end;
hence  LSeg ((((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),1)) + ((GoB f) * ((len (GoB f)),2)))) + |[1,0]|)) misses L~ f by Th22; ::_thesis: verum
end;

theorem :: GOBOARD8:36
for f being non constant standard special_circular_sequence holds 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
proof
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:32;
now__::_thesis:_for_p_being_Point_of_(TOP-REAL_2)_st_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]|))_holds_
p_`1_>_((GoB_f)_*_((len_(GoB_f)),1))_`1
A2: 1 < width (GoB f) by GOBOARD7:33;
then A3: ((width (GoB f)) -' 1) + 1 = width (GoB f) by XREAL_1:235;
then A4: (width (GoB f)) -' 1 <= width (GoB f) by NAT_1:11;
A5: ((GoB f) * ((len (GoB f)),(width (GoB f)))) `1 = ((GoB f) * ((len (GoB f)),1)) `1 by A1, A2, GOBOARD5:2;
then (((GoB f) * ((len (GoB f)),(width (GoB f)))) + |[1,1]|) `1 = (((GoB f) * ((len (GoB f)),1)) `1) + (|[1,1]| `1) by TOPREAL3:2
.= (((GoB f) * ((len (GoB f)),1)) `1) + 1 by EUCLID:52 ;
then A6: ((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:53;
 1 <= (width (GoB f)) -' 1 by A2, A3, NAT_1:13;
then A7: ((GoB f) * ((len (GoB f)),((width (GoB f)) -' 1))) `1 = ((GoB f) * ((len (GoB f)),1)) `1 by A1, A4, GOBOARD5:2;
(((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:2
.= ((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:4
.= ((1 / 2) * ((((GoB f) * ((len (GoB f)),1)) `1) + (((GoB f) * ((len (GoB f)),1)) `1))) + (|[1,0]| `1) by A7, A5, TOPREAL3:2
.= (1 * (((GoB f) * ((len (GoB f)),1)) `1)) + 1 by EUCLID:52 ;
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:53;
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  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
then  p `1 = (((GoB f) * ((len (GoB f)),1)) `1) + 1 by A8, A6, TOPREAL3:11;
hence  p `1 > ((GoB f) * ((len (GoB f)),1)) `1 by XREAL_1:29; ::_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
end;

theorem :: GOBOARD8:37
for k being Element of NAT
for f being non constant standard special_circular_sequence st 1 <= k & k + 1 <= len f holds
Int (left_cell (f,k)) misses L~ f
proof
let k be Element of NAT ; ::_thesis: for f being non constant standard special_circular_sequence st 1 <= k & k + 1 <= len f holds
Int (left_cell (f,k)) misses L~ f
let f be non constant standard special_circular_sequence; ::_thesis: ( 1 <= k & k + 1 <= len f implies Int (left_cell (f,k)) misses L~ f )
assume that
A1: 1 <= k and
A2: k + 1 <= len f ; ::_thesis: Int (left_cell (f,k)) misses L~ f
 k <= k + 1 by NAT_1:11;
then  k <= len f by A2, XXREAL_0:2;
then A3: k in dom f by A1, FINSEQ_3:25;
then consider i1, j1 being Element of NAT  such that
A4: [i1,j1] in Indices (GoB f) and
A5: f /. k = (GoB f) * (i1,j1) by GOBOARD2:14;
A6: i1 <= len (GoB f) by A4, MATRIX_1:38;
 j1 <> 0 by A4, MATRIX_1:38;
then consider j being Nat such that
A7: j1 = j + 1 by NAT_1:6;
 i1 <> 0 by A4, MATRIX_1:38;
then consider i being Nat such that
A8: i1 = i + 1 by NAT_1:6;
 i <= i1 by A8, NAT_1:11;
then A9: i <= len (GoB f) by A6, XXREAL_0:2;
A10: j1 <= width (GoB f) by A4, MATRIX_1:38;
 k + 1 >= 1 by NAT_1:11;
then A11: k + 1 in dom f by A2, FINSEQ_3:25;
then consider i2, j2 being Element of NAT  such that
A12: [i2,j2] in Indices (GoB f) and
A13: f /. (k + 1) = (GoB f) * (i2,j2) by GOBOARD2:14;
reconsider i19 = i1, i29 = i2, j19 = j1, j29 = j2 as Element of REAL by XREAL_0:def_1;
 (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A3, A4, A5, A11, A12, A13, GOBOARD5:12;
then A14: ( ( abs (i19 - i29) = 1 & j1 = j2 ) or ( abs (j19 - j29) = 1 & i1 = i2 ) ) by SEQM_3:42;
reconsider i = i, j = j as Element of NAT by ORDINAL1:def_12;
A15: i1 = i + 1 by A8;
A16: j1 = j + 1 by A7;
A17: j2 <= width (GoB f) by A12, MATRIX_1:38;
A18: i2 <= len (GoB f) by A12, MATRIX_1:38;
 j <= j1 by A7, NAT_1:11;
then A19: j <= width (GoB f) by A10, XXREAL_0:2;
percases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A14, SEQM_3:41;
suppose ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: Int (left_cell (f,k)) misses L~ f
then  left_cell (f,k) = cell ((GoB f),i,j1) by A1, A2, A4, A5, A8, A12, A13, GOBOARD5:27;
hence  Int (left_cell (f,k)) misses L~ f by A10, A9, GOBOARD7:12; ::_thesis: verum
end;
suppose ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: Int (left_cell (f,k)) misses L~ f
then  left_cell (f,k) = cell ((GoB f),i1,j1) by A1, A2, A4, A5, A16, A12, A13, GOBOARD5:28;
hence  Int (left_cell (f,k)) misses L~ f by A6, A10, GOBOARD7:12; ::_thesis: verum
end;
suppose ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: Int (left_cell (f,k)) misses L~ f
then  left_cell (f,k) = cell ((GoB f),i2,j) by A1, A2, A4, A5, A7, A12, A13, GOBOARD5:29;
hence  Int (left_cell (f,k)) misses L~ f by A19, A18, GOBOARD7:12; ::_thesis: verum
end;
suppose ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: Int (left_cell (f,k)) misses L~ f
then  left_cell (f,k) = cell ((GoB f),i1,j2) by A1, A2, A4, A5, A15, A12, A13, GOBOARD5:30;
hence  Int (left_cell (f,k)) misses L~ f by A6, A17, GOBOARD7:12; ::_thesis: verum
end;
end;
end;

theorem :: GOBOARD8:38
for k being Element of NAT
for f being non constant standard special_circular_sequence st 1 <= k & k + 1 <= len f holds
Int (right_cell (f,k)) misses L~ f
proof
let k be Element of NAT ; ::_thesis: for f being non constant standard special_circular_sequence st 1 <= k & k + 1 <= len f holds
Int (right_cell (f,k)) misses L~ f
let f be non constant standard special_circular_sequence; ::_thesis: ( 1 <= k & k + 1 <= len f implies Int (right_cell (f,k)) misses L~ f )
assume that
A1: 1 <= k and
A2: k + 1 <= len f ; ::_thesis: Int (right_cell (f,k)) misses L~ f
 k <= k + 1 by NAT_1:11;
then  k <= len f by A2, XXREAL_0:2;
then A3: k in dom f by A1, FINSEQ_3:25;
then consider i1, j1 being Element of NAT  such that
A4: [i1,j1] in Indices (GoB f) and
A5: f /. k = (GoB f) * (i1,j1) by GOBOARD2:14;
A6: i1 <= len (GoB f) by A4, MATRIX_1:38;
 j1 <> 0 by A4, MATRIX_1:38;
then consider j being Nat such that
A7: j1 = j + 1 by NAT_1:6;
 i1 <> 0 by A4, MATRIX_1:38;
then consider i being Nat such that
A8: i1 = i + 1 by NAT_1:6;
 i <= i1 by A8, NAT_1:11;
then A9: i <= len (GoB f) by A6, XXREAL_0:2;
A10: j1 <= width (GoB f) by A4, MATRIX_1:38;
 k + 1 >= 1 by NAT_1:11;
then A11: k + 1 in dom f by A2, FINSEQ_3:25;
then consider i2, j2 being Element of NAT  such that
A12: [i2,j2] in Indices (GoB f) and
A13: f /. (k + 1) = (GoB f) * (i2,j2) by GOBOARD2:14;
reconsider i19 = i1, i29 = i2, j19 = j1, j29 = j2 as Element of REAL by XREAL_0:def_1;
 (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A3, A4, A5, A11, A12, A13, GOBOARD5:12;
then A14: ( ( abs (i19 - i29) = 1 & j1 = j2 ) or ( abs (j19 - j29) = 1 & i1 = i2 ) ) by SEQM_3:42;
reconsider i = i, j = j as Element of NAT by ORDINAL1:def_12;
A15: i1 = i + 1 by A8;
A16: j1 = j + 1 by A7;
A17: j2 <= width (GoB f) by A12, MATRIX_1:38;
A18: i2 <= len (GoB f) by A12, MATRIX_1:38;
 j <= j1 by A7, NAT_1:11;
then A19: j <= width (GoB f) by A10, XXREAL_0:2;
percases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A14, SEQM_3:41;
suppose ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: Int (right_cell (f,k)) misses L~ f
then  right_cell (f,k) = cell ((GoB f),i1,j1) by A1, A2, A4, A5, A15, A12, A13, GOBOARD5:27;
hence  Int (right_cell (f,k)) misses L~ f by A6, A10, GOBOARD7:12; ::_thesis: verum
end;
suppose ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: Int (right_cell (f,k)) misses L~ f
then  right_cell (f,k) = cell ((GoB f),i1,j) by A1, A2, A4, A5, A7, A12, A13, GOBOARD5:28;
hence  Int (right_cell (f,k)) misses L~ f by A6, A19, GOBOARD7:12; ::_thesis: verum
end;
suppose ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: Int (right_cell (f,k)) misses L~ f
then  right_cell (f,k) = cell ((GoB f),i2,j1) by A1, A2, A4, A5, A16, A12, A13, GOBOARD5:29;
hence  Int (right_cell (f,k)) misses L~ f by A10, A18, GOBOARD7:12; ::_thesis: verum
end;
suppose ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: Int (right_cell (f,k)) misses L~ f
then  right_cell (f,k) = cell ((GoB f),i,j2) by A1, A2, A4, A5, A8, A12, A13, GOBOARD5:30;
hence  Int (right_cell (f,k)) misses L~ f by A9, A17, GOBOARD7:12; ::_thesis: verum
end;
end;
end;