theorem Th21: :: MENELAUS:21

for A, B, C, A1, B1, C1 being Point of (TOP-REAL 2)
for lambda, mu, nu being Real st A,B,C is_a_triangle & A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & C1 = ((1 - nu) * A) + (nu * B) & lambda <> 1 & mu <> 1 & nu <> 1 & (1 - mu) + (lambda * mu) <> 0 & (1 - lambda) + (nu * lambda) <> 0 & (1 - nu) + (mu * nu) <> 0 holds
( ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff ex A2 being Point of (TOP-REAL 2) st
( A,A1,A2 are_collinear & B,B1,A2 are_collinear & C,C1,A2 are_collinear ) )