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) `))) = (cell ((GoB f),i,j)) /\ ((L~ f) `)
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) `))) = (cell ((GoB f),i,j)) /\ ((L~ f) `) )
reconsider V = Int (cell ((GoB f),i,j)) as Subset of (TOP-REAL 2) ;
reconsider B = (L~ f) ` as Subset of (TOP-REAL 2) ;
assume A1: ( i <= len (GoB f) & j <= width (GoB f) ) ; :: thesis: Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `))) = (cell ((GoB f),i,j)) /\ ((L~ f) `)
then Cl (Down (V,B)) = (Cl V) /\ B by Th1, CONNSP_3:29;
hence Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `))) = (cell ((GoB f),i,j)) /\ ((L~ f) `) by A1, GOBRD11:35; :: thesis: verum