let f be non constant standard special_circular_sequence; 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; ( 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) )
; ( 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; 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; verum