:: deftheorem defines is_in_general_position_wrt JORDAN12:def 1 :
for n being Nat
for f1, f2 being FinSequence of (TOP-REAL n) holds
( f1 is_in_general_position_wrt f2 iff ( L~ f1 misses rng f2 & ( for i being Nat st 1 <= i & i < len f2 holds
(L~ f1) /\ (LSeg (f2,i)) is trivial ) ) );