let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle implies median (A,B,C) is being_line )
assume A1: A,B,C is_a_triangle ; :: thesis: median (A,B,C) is being_line
A2: A,B,C are_mutually_distinct by A1, EUCLID_6:20;
assume not median (A,B,C) is being_line ; :: thesis: contradiction
then consider x being Element of REAL 2 such that
A3: median (A,B,C) = {x} by Th6;
set D = the_midpoint_of_the_segment (B,C);
( A in median (A,B,C) & the_midpoint_of_the_segment (B,C) in median (A,B,C) ) by EUCLID_4:41;
then ( A = x & the_midpoint_of_the_segment (B,C) = x ) by A3, TARSKI:def 1;
then ( A in LSeg (B,C) & LSeg (B,C) c= Line (B,C) ) by Th21, RLTOPSP1:73;
hence contradiction by A1, A2, MENELAUS:13; :: thesis: verum