let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle implies ex D being Point of (TOP-REAL 2) st
( D in median (A,B,C) & D in median (B,C,A) & D in median (C,A,B) ) )
assume A1: A,B,C is_a_triangle ; :: thesis: ex D being Point of (TOP-REAL 2) st
( D in median (A,B,C) & D in median (B,C,A) & D in median (C,A,B) )
set D = the_midpoint_of_the_segment (B,C);
set E = the_midpoint_of_the_segment (C,A);
set F = the_midpoint_of_the_segment (A,B);
A2: now :: thesis: ( the_midpoint_of_the_segment (B,C) = ((1 - (1 / 2)) * B) + ((1 / 2) * C) & the_midpoint_of_the_segment (C,A) = ((1 - (1 / 2)) * C) + ((1 / 2) * A) & the_midpoint_of_the_segment (A,B) = ((1 - (1 / 2)) * A) + ((1 / 2) * B) )
thus the_midpoint_of_the_segment (B,C) = (1 / 2) * (B + C) by Th22
.= ((1 - (1 / 2)) * B) + ((1 / 2) * C) by RLVECT_1:def 5 ; :: thesis: ( the_midpoint_of_the_segment (C,A) = ((1 - (1 / 2)) * C) + ((1 / 2) * A) & the_midpoint_of_the_segment (A,B) = ((1 - (1 / 2)) * A) + ((1 / 2) * B) )
thus the_midpoint_of_the_segment (C,A) = (1 / 2) * (C + A) by Th22
.= ((1 - (1 / 2)) * C) + ((1 / 2) * A) by RLVECT_1:def 5 ; :: thesis: the_midpoint_of_the_segment (A,B) = ((1 - (1 / 2)) * A) + ((1 / 2) * B)
thus the_midpoint_of_the_segment (A,B) = (1 / 2) * (A + B) by Th22
.= ((1 - (1 / 2)) * A) + ((1 / 2) * B) by RLVECT_1:def 5 ; :: thesis: verum
end;
then A3: Line (A,(the_midpoint_of_the_segment (B,C))), Line (B,(the_midpoint_of_the_segment (C,A))), Line (C,(the_midpoint_of_the_segment (A,B))) are_concurrent by A1, Th59;
reconsider rA = A, rD = the_midpoint_of_the_segment (B,C), rB = B, rC = C, rE = the_midpoint_of_the_segment (C,A), rF = the_midpoint_of_the_segment (A,B) as Element of REAL 2 by EUCLID:22;
( Line (rA,rD) = Line (A,(the_midpoint_of_the_segment (B,C))) & Line (rB,rE) = Line (B,(the_midpoint_of_the_segment (C,A))) & Line (rC,rF) = Line (C,(the_midpoint_of_the_segment (A,B))) ) by Th4;
then reconsider LAD = Line (A,(the_midpoint_of_the_segment (B,C))), LBE = Line (B,(the_midpoint_of_the_segment (C,A))), LCF = Line (C,(the_midpoint_of_the_segment (A,B))) as Subset of (REAL 2) ;
now :: thesis: ( Line (A,(the_midpoint_of_the_segment (B,C))) is_parallel_to Line (B,(the_midpoint_of_the_segment (C,A))) & Line (B,(the_midpoint_of_the_segment (C,A))) is_parallel_to Line (C,(the_midpoint_of_the_segment (A,B))) implies not Line (C,(the_midpoint_of_the_segment (A,B))) is_parallel_to Line (A,(the_midpoint_of_the_segment (B,C))) )
assume A5: ( Line (A,(the_midpoint_of_the_segment (B,C))) is_parallel_to Line (B,(the_midpoint_of_the_segment (C,A))) & Line (B,(the_midpoint_of_the_segment (C,A))) is_parallel_to Line (C,(the_midpoint_of_the_segment (A,B))) & Line (C,(the_midpoint_of_the_segment (A,B))) is_parallel_to Line (A,(the_midpoint_of_the_segment (B,C))) ) ; :: thesis: contradiction
( the_midpoint_of_the_segment (A,B) = ((1 - (1 / 2)) * A) + ((1 / 2) * B) & the_midpoint_of_the_segment (B,C) = ((1 - (1 / 2)) * B) + ((1 / 2) * C) & (1 - (1 / 2)) + (((1 / 2) * 1) / 2) <> 0 & C,A,B is_a_triangle ) by A1, A2, MENELAUS:15;
hence contradiction by A5, MENELAUS:16; :: thesis: verum
end;
hence ex D being Point of (TOP-REAL 2) st
( D in median (A,B,C) & D in median (B,C,A) & D in median (C,A,B) ) by A3, MENELAUS:def 1; :: thesis: verum