theorem :: JORDAN5B:26

for f being constant standard special_circular_sequence
for i, j being Nat st 1 <= i & j <= width (GoB f) & i < j holds
(LSeg (((GoB f) * ((len (GoB f)),1)),((GoB f) * ((len (GoB f)),i)))) /\ (LSeg (((GoB f) * ((len (GoB f)),j)),((GoB f) * ((len (GoB f)),(width (GoB f)))))) = {}