let f be non constant standard special_circular_sequence; :: thesis: for i, j being 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 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 convex & Down ((Int (cell ((GoB f),i,j))),((L~ f) `)) = Int (cell ((GoB f),i,j)) ) by Th1, GOBOARD9:17, XBOOLE_1:28;
then Down ((Int (cell ((GoB f),i,j))),((L~ f) `)) is connected by CONNSP_1:23;
hence Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `))) is connected by CONNSP_1:19; :: 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, Th1, XBOOLE_1:28; :: thesis: verum