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);

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) ;

( 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

( 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) )

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;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;.= ((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

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))) )

hence
ex D being Point of (TOP-REAL 2) st 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;( 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

( 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