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

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