let f be non constant standard special_circular_sequence; :: thesis: for k being Element of NAT st 1 <= k & k + 1 <= len f holds
Int (left_cell f,k) <> {}
let k be Element of 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 Element of NAT st
( i <= len (GoB f) & j <= width (GoB f) & cell (GoB f),i,j = left_cell f,k ) by A1, A2, Th14;
hence Int (left_cell f,k) <> {} by Th17; :: thesis: verum