theorem :: JORDAN5B:25

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