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

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