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