theorem Th9: :: JORDAN12:9

for f1, f2 being FinSequence of (TOP-REAL 2) st f1,f2 are_in_general_position holds
for i, j being Nat st 1 <= i & i + 1 <= len f1 & 1 <= j & j + 1 <= len f2 holds
(LSeg (f1,i)) /\ (LSeg (f2,j)) is trivial