theorem Th36: :: JORDAN5D:36

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 `2 = ((GoB h) * (i,j)) `2 & q in L~ h )