theorem Th35: :: JORDAN5D:35

for h being non constant standard special_circular_sequence
for i, j being Nat st 1 <= i & i <= len (GoB h) & 1 <= j & j <= width (GoB h) holds
ex q being Point of (TOP-REAL 2) st
( q `1 = ((GoB h) * (i,j)) `1 & q in L~ h )