for A, B, C, D, E, F being Point of (TOP-REAL 2) st 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) holds
Line (A,D), Line (B,E), Line (C,F) are_concurrent