theorem
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 holds
(
((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff
Line (
A,
A1),
Line (
B,
B1),
Line (
C,
C1)
are_concurrent )