let f be non constant standard special_circular_sequence; :: thesis: for i, j being Element of NAT st i <= len (GoB f) & j <= width (GoB f) holds
Int (cell ((GoB f),i,j)) c= (L~ f) `
let i, j be Element of NAT ; :: thesis: ( i <= len (GoB f) & j <= width (GoB f) implies Int (cell ((GoB f),i,j)) c= (L~ f) ` )
assume ( i <= len (GoB f) & j <= width (GoB f) ) ; :: thesis: Int (cell ((GoB f),i,j)) c= (L~ f) `
then Int (cell ((GoB f),i,j)) misses L~ f by GOBOARD7:12;
hence Int (cell ((GoB f),i,j)) c= (L~ f) ` by SUBSET_1:23; :: thesis: verum