let f be non constant standard special_circular_sequence; :: thesis: for k being Nat st 1 <= k & k + 1 <= len f holds

Int (left_cell (f,k)) <> {}

let k be Nat; :: thesis: ( 1 <= k & k + 1 <= len f implies Int (left_cell (f,k)) <> {} )

assume that

A1: 1 <= k and

A2: k + 1 <= len f ; :: thesis: Int (left_cell (f,k)) <> {}

ex i, j being Nat st

( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) ) by A1, A2, Th10;

hence Int (left_cell (f,k)) <> {} by Th13; :: thesis: verum

Int (left_cell (f,k)) <> {}

let k be Nat; :: thesis: ( 1 <= k & k + 1 <= len f implies Int (left_cell (f,k)) <> {} )

assume that

A1: 1 <= k and

A2: k + 1 <= len f ; :: thesis: Int (left_cell (f,k)) <> {}

ex i, j being Nat st

( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) ) by A1, A2, Th10;

hence Int (left_cell (f,k)) <> {} by Th13; :: thesis: verum