let A, B, C, D, E, F be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle & D = ((1 - (1 / 2)) * B) + ((1 / 2) * C) & E = ((1 - (1 / 2)) * C) + ((1 / 2) * A) & F = ((1 - (1 / 2)) * A) + ((1 / 2) * B) implies Line (A,D), Line (B,E), Line (C,F) are_concurrent )
assume that
A1: A,B,C is_a_triangle and
A2: D = ((1 - (1 / 2)) * B) + ((1 / 2) * C) and
A3: E = ((1 - (1 / 2)) * C) + ((1 / 2) * A) and
A4: F = ((1 - (1 / 2)) * A) + ((1 / 2) * B) ; :: thesis: Line (A,D), Line (B,E), Line (C,F) are_concurrent
set lambda = 1 / 2;
set mu = 1 / 2;
set nu = 1 / 2;
(((1 / 2) / (1 - (1 / 2))) * ((1 / 2) / (1 - (1 / 2)))) * ((1 / 2) / (1 - (1 / 2))) = 1 ;
hence Line (A,D), Line (B,E), Line (C,F) are_concurrent by A1, A2, A3, A4, MENELAUS:22; :: thesis: verum