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
( Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `))) is connected & Down ((Int (cell ((GoB f),i,j))),((L~ f) `)) = Int (cell ((GoB f),i,j)) )
let i, j be Element of NAT ; :: thesis: ( i <= len (GoB f) & j <= width (GoB f) implies ( Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `))) is connected & Down ((Int (cell ((GoB f),i,j))),((L~ f) `)) = Int (cell ((GoB f),i,j)) ) )
assume A1: ( i <= len (GoB f) & j <= width (GoB f) ) ; :: thesis: ( Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `))) is connected & Down ((Int (cell ((GoB f),i,j))),((L~ f) `)) = Int (cell ((GoB f),i,j)) )
then ( Int (cell ((GoB f),i,j)) is connected & Down ((Int (cell ((GoB f),i,j))),((L~ f) `)) = Int (cell ((GoB f),i,j)) ) by Th2, GOBOARD9:21, XBOOLE_1:28;
then Down ((Int (cell ((GoB f),i,j))),((L~ f) `)) is connected by CONNSP_1:24;
hence Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `))) is connected by CONNSP_1:20; :: thesis: Down ((Int (cell ((GoB f),i,j))),((L~ f) `)) = Int (cell ((GoB f),i,j))
thus Down ((Int (cell ((GoB f),i,j))),((L~ f) `)) = Int (cell ((GoB f),i,j)) by A1, Th2, XBOOLE_1:28; :: thesis: verum