theorem Th3: :: GOBRD12:3

for f being 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)) )