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