let A, B, C, A1, B1 be 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) )
let lambda, mu be Real; ( A,B,C is_a_triangle & A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & mu <> 1 implies ( (1 - mu) + (lambda * mu) <> 0 iff not Line (A,A1) is_parallel_to Line (B,B1) ) )
assume that
A1:
A,B,C is_a_triangle
and
A2:
A1 = ((1 - lambda) * B) + (lambda * C)
and
A3:
B1 = ((1 - mu) * C) + (mu * A)
and
A4:
mu <> 1
; ( (1 - mu) + (lambda * mu) <> 0 iff not Line (A,A1) is_parallel_to Line (B,B1) )
A5:
A <> A1
by A1, A2, Th14;
B,C,A is_a_triangle
by A1;
then A6:
B <> B1
by A3, Th14;
hereby ( not Line (A,A1) is_parallel_to Line (B,B1) implies (1 - mu) + (lambda * mu) <> 0 )
assume
(1 - mu) + (lambda * mu) <> 0
;
not Line (A,A1) is_parallel_to Line (B,B1)then consider C2 being
Point of
(TOP-REAL 2) such that A7:
(
A,
A1,
C2 are_collinear &
B,
B1,
C2 are_collinear )
by Lm3, A1, A2, A3;
(
C2,
A,
A1 are_collinear &
C2,
B,
B1 are_collinear )
by A7;
then
(
C2 in Line (
A,
A1) &
C2 in Line (
B,
B1) )
by A5, A6, Th13;
hence
not
Line (
A,
A1)
is_parallel_to Line (
B,
B1)
by XBOOLE_0:3;
verum
end;
assume
not Line (A,A1) is_parallel_to Line (B,B1)
; (1 - mu) + (lambda * mu) <> 0
then consider C2 being object such that
A8:
( C2 in Line (A,A1) & C2 in Line (B,B1) )
by XBOOLE_0:3;
reconsider C2 = C2 as Point of (TOP-REAL 2) by A8;
( C2,A,A1 are_collinear & C2,B,B1 are_collinear )
by A8, A5, A6, Th13;
then
( A,A1,C2 are_collinear & B,B1,C2 are_collinear )
;
hence
(1 - mu) + (lambda * mu) <> 0
by Lm2, A1, A2, A3, A4; verum