theorem Th16: :: MENELAUS:16

for A, B, C, A1, B1 being Point of (TOP-REAL 2)
for lambda, mu being Real st A,B,C is_a_triangle & A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & mu <> 1 holds
( (1 - mu) + (lambda * mu) <> 0 iff not Line (A,A1) is_parallel_to Line (B,B1) )