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

( (median (A,B,C)) /\ (median (B,C,A)) = {D} & (median (B,C,A)) /\ (median (C,A,B)) = {D} & (median (C,A,B)) /\ (median (A,B,C)) = {D} ) )

assume A1: A,B,C is_a_triangle ; :: thesis: ex D being Point of (TOP-REAL 2) st

( (median (A,B,C)) /\ (median (B,C,A)) = {D} & (median (B,C,A)) /\ (median (C,A,B)) = {D} & (median (C,A,B)) /\ (median (A,B,C)) = {D} )

then consider D being Point of (TOP-REAL 2) such that

A2: D in median (A,B,C) and

A3: D in median (B,C,A) and

A4: D in median (C,A,B) by Th62;

A5: A,B,C are_mutually_distinct by A1, EUCLID_6:20;

reconsider rA = A, rB = B, rC = C, rBC = the_midpoint_of_the_segment (B,C), rCA = the_midpoint_of_the_segment (C,A), rAB = the_midpoint_of_the_segment (A,B) as Element of REAL 2 by EUCLID:22;

reconsider L1 = Line (rA,rBC), L2 = Line (rB,rCA), L3 = Line (rC,rAB) as Element of line_of_REAL 2 by EUCLIDLP:47;

A6: ( B,C,A is_a_triangle & C,B,A is_a_triangle ) by A1, MENELAUS:15;

A7: C,A,B is_a_triangle by A1, MENELAUS:15;

A8: ( L1 = Line (A,(the_midpoint_of_the_segment (B,C))) & L2 = Line (B,(the_midpoint_of_the_segment (C,A))) & L3 = Line (C,(the_midpoint_of_the_segment (A,B))) ) by Th4;

then A9: ( L1 is being_line & L2 is being_line & L3 is being_line ) by A1, A2, A3, A4, A6, A7, Th61;

( D in L1 & D in L2 & D in L3 ) by A2, A3, A4, Th4;

then A10: ( D in L1 /\ L2 & D in L1 /\ L3 & D in L2 /\ L3 ) by XBOOLE_0:def 4;

A14: L1 /\ L2 = {x} by Th16;

A18: L1 /\ L3 = {y} by Th16;

A22: L2 /\ L3 = {z} by Th16;

( D = x & D = y & D = z ) by A10, A14, A18, A22, TARSKI:def 1;

hence ex D being Point of (TOP-REAL 2) st

( (median (A,B,C)) /\ (median (B,C,A)) = {D} & (median (B,C,A)) /\ (median (C,A,B)) = {D} & (median (C,A,B)) /\ (median (A,B,C)) = {D} ) by A14, A18, A22, A8; :: thesis: verum

( (median (A,B,C)) /\ (median (B,C,A)) = {D} & (median (B,C,A)) /\ (median (C,A,B)) = {D} & (median (C,A,B)) /\ (median (A,B,C)) = {D} ) )

assume A1: A,B,C is_a_triangle ; :: thesis: ex D being Point of (TOP-REAL 2) st

( (median (A,B,C)) /\ (median (B,C,A)) = {D} & (median (B,C,A)) /\ (median (C,A,B)) = {D} & (median (C,A,B)) /\ (median (A,B,C)) = {D} )

then consider D being Point of (TOP-REAL 2) such that

A2: D in median (A,B,C) and

A3: D in median (B,C,A) and

A4: D in median (C,A,B) by Th62;

A5: A,B,C are_mutually_distinct by A1, EUCLID_6:20;

reconsider rA = A, rB = B, rC = C, rBC = the_midpoint_of_the_segment (B,C), rCA = the_midpoint_of_the_segment (C,A), rAB = the_midpoint_of_the_segment (A,B) as Element of REAL 2 by EUCLID:22;

reconsider L1 = Line (rA,rBC), L2 = Line (rB,rCA), L3 = Line (rC,rAB) as Element of line_of_REAL 2 by EUCLIDLP:47;

A6: ( B,C,A is_a_triangle & C,B,A is_a_triangle ) by A1, MENELAUS:15;

A7: C,A,B is_a_triangle by A1, MENELAUS:15;

A8: ( L1 = Line (A,(the_midpoint_of_the_segment (B,C))) & L2 = Line (B,(the_midpoint_of_the_segment (C,A))) & L3 = Line (C,(the_midpoint_of_the_segment (A,B))) ) by Th4;

then A9: ( L1 is being_line & L2 is being_line & L3 is being_line ) by A1, A2, A3, A4, A6, A7, Th61;

( D in L1 & D in L2 & D in L3 ) by A2, A3, A4, Th4;

then A10: ( D in L1 /\ L2 & D in L1 /\ L3 & D in L2 /\ L3 ) by XBOOLE_0:def 4;

now :: thesis: ( not L1 // L2 & L1 is being_line & L2 is being_line & not L1 is being_point & not L2 is being_point )

then consider x being Element of REAL 2 such that
L1 <> L2

thus ( L1 is being_line & L2 is being_line & not L1 is being_point & not L2 is being_point ) by A8, A1, A2, A3, A6, Th61, Th7; :: thesis: verum

end;proof

hence
not L1 // L2
by A10, XBOOLE_0:4, EUCLIDLP:71; :: thesis: ( L1 is being_line & L2 is being_line & not L1 is being_point & not L2 is being_point )
assume A11:
L1 = L2
; :: thesis: contradiction

A12: ( A in Line (A,(the_midpoint_of_the_segment (B,C))) & the_midpoint_of_the_segment (B,C) in Line (A,(the_midpoint_of_the_segment (B,C))) & B in Line (B,(the_midpoint_of_the_segment (C,A))) & the_midpoint_of_the_segment (C,A) in Line (B,(the_midpoint_of_the_segment (C,A))) & C in Line (C,(the_midpoint_of_the_segment (A,B))) & the_midpoint_of_the_segment (A,B) in Line (C,(the_midpoint_of_the_segment (A,B))) ) by RLTOPSP1:72;

( A in L1 & B in L1 & A in L2 & B in L2 & the_midpoint_of_the_segment (B,C) in L1 & the_midpoint_of_the_segment (B,C) in L2 & the_midpoint_of_the_segment (C,A) in L1 & the_midpoint_of_the_segment (C,A) in L2 ) by A12, A11, Th4;

then L1 = Line (rA,rB) by A5, A9, EUCLIDLP:30;

then A13: L1 = Line (A,B) by Th4;

( B <> the_midpoint_of_the_segment (B,C) & B in L1 & the_midpoint_of_the_segment (B,C) in LSeg (B,C) & the_midpoint_of_the_segment (B,C) in L1 & L1 is being_line ) by A2, A8, A1, Th61, RLTOPSP1:72, A11, Th21, A5, Th25;

then ( A in L1 & B in L1 & C in L1 ) by A12, Th4, Th5;

then C,A,B are_collinear by A13, A5, MENELAUS:13;

hence contradiction by A1, MENELAUS:15; :: thesis: verum

end;A12: ( A in Line (A,(the_midpoint_of_the_segment (B,C))) & the_midpoint_of_the_segment (B,C) in Line (A,(the_midpoint_of_the_segment (B,C))) & B in Line (B,(the_midpoint_of_the_segment (C,A))) & the_midpoint_of_the_segment (C,A) in Line (B,(the_midpoint_of_the_segment (C,A))) & C in Line (C,(the_midpoint_of_the_segment (A,B))) & the_midpoint_of_the_segment (A,B) in Line (C,(the_midpoint_of_the_segment (A,B))) ) by RLTOPSP1:72;

( A in L1 & B in L1 & A in L2 & B in L2 & the_midpoint_of_the_segment (B,C) in L1 & the_midpoint_of_the_segment (B,C) in L2 & the_midpoint_of_the_segment (C,A) in L1 & the_midpoint_of_the_segment (C,A) in L2 ) by A12, A11, Th4;

then L1 = Line (rA,rB) by A5, A9, EUCLIDLP:30;

then A13: L1 = Line (A,B) by Th4;

( B <> the_midpoint_of_the_segment (B,C) & B in L1 & the_midpoint_of_the_segment (B,C) in LSeg (B,C) & the_midpoint_of_the_segment (B,C) in L1 & L1 is being_line ) by A2, A8, A1, Th61, RLTOPSP1:72, A11, Th21, A5, Th25;

then ( A in L1 & B in L1 & C in L1 ) by A12, Th4, Th5;

then C,A,B are_collinear by A13, A5, MENELAUS:13;

hence contradiction by A1, MENELAUS:15; :: thesis: verum

thus ( L1 is being_line & L2 is being_line & not L1 is being_point & not L2 is being_point ) by A8, A1, A2, A3, A6, Th61, Th7; :: thesis: verum

A14: L1 /\ L2 = {x} by Th16;

now :: thesis: ( not L1 // L3 & L1 is being_line & L3 is being_line & not L1 is being_point & not L3 is being_point )

then consider y being Element of REAL 2 such that
L1 <> L3

thus ( L1 is being_line & L3 is being_line & not L1 is being_point & not L3 is being_point ) by A2, A4, A8, A1, A7, Th61, Th7; :: thesis: verum

end;proof

hence
not L1 // L3
by A10, XBOOLE_0:4, EUCLIDLP:71; :: thesis: ( L1 is being_line & L3 is being_line & not L1 is being_point & not L3 is being_point )
assume A15:
L1 = L3
; :: thesis: contradiction

A16: ( A in Line (A,(the_midpoint_of_the_segment (B,C))) & the_midpoint_of_the_segment (B,C) in Line (A,(the_midpoint_of_the_segment (B,C))) & B in Line (B,(the_midpoint_of_the_segment (C,A))) & the_midpoint_of_the_segment (C,A) in Line (B,(the_midpoint_of_the_segment (C,A))) & C in Line (C,(the_midpoint_of_the_segment (A,B))) & the_midpoint_of_the_segment (A,B) in Line (C,(the_midpoint_of_the_segment (A,B))) ) by RLTOPSP1:72;

( A in L1 & C in L1 & A in L3 & C in L3 & the_midpoint_of_the_segment (B,C) in L1 & the_midpoint_of_the_segment (B,C) in L3 & the_midpoint_of_the_segment (A,B) in L1 & the_midpoint_of_the_segment (A,B) in L3 ) by A15, Th4, A16;

then L1 = Line (rA,rC) by A5, A9, EUCLIDLP:30;

then A17: L1 = Line (A,C) by Th4;

( A <> the_midpoint_of_the_segment (A,B) & A in L1 & the_midpoint_of_the_segment (A,B) in LSeg (A,B) & the_midpoint_of_the_segment (A,B) in L1 & L1 is being_line ) by A2, A5, Th25, A8, A1, Th61, A15, RLTOPSP1:72, Th21;

then ( A in L1 & C in L1 & B in L1 ) by A16, A15, Th4, Th5;

then B,A,C are_collinear by A17, A5, MENELAUS:13;

hence contradiction by A1, MENELAUS:15; :: thesis: verum

end;A16: ( A in Line (A,(the_midpoint_of_the_segment (B,C))) & the_midpoint_of_the_segment (B,C) in Line (A,(the_midpoint_of_the_segment (B,C))) & B in Line (B,(the_midpoint_of_the_segment (C,A))) & the_midpoint_of_the_segment (C,A) in Line (B,(the_midpoint_of_the_segment (C,A))) & C in Line (C,(the_midpoint_of_the_segment (A,B))) & the_midpoint_of_the_segment (A,B) in Line (C,(the_midpoint_of_the_segment (A,B))) ) by RLTOPSP1:72;

( A in L1 & C in L1 & A in L3 & C in L3 & the_midpoint_of_the_segment (B,C) in L1 & the_midpoint_of_the_segment (B,C) in L3 & the_midpoint_of_the_segment (A,B) in L1 & the_midpoint_of_the_segment (A,B) in L3 ) by A15, Th4, A16;

then L1 = Line (rA,rC) by A5, A9, EUCLIDLP:30;

then A17: L1 = Line (A,C) by Th4;

( A <> the_midpoint_of_the_segment (A,B) & A in L1 & the_midpoint_of_the_segment (A,B) in LSeg (A,B) & the_midpoint_of_the_segment (A,B) in L1 & L1 is being_line ) by A2, A5, Th25, A8, A1, Th61, A15, RLTOPSP1:72, Th21;

then ( A in L1 & C in L1 & B in L1 ) by A16, A15, Th4, Th5;

then B,A,C are_collinear by A17, A5, MENELAUS:13;

hence contradiction by A1, MENELAUS:15; :: thesis: verum

thus ( L1 is being_line & L3 is being_line & not L1 is being_point & not L3 is being_point ) by A2, A4, A8, A1, A7, Th61, Th7; :: thesis: verum

A18: L1 /\ L3 = {y} by Th16;

now :: thesis: ( not L2 // L3 & L2 is being_line & L3 is being_line & not L2 is being_point & not L3 is being_point )

then consider z being Element of REAL 2 such that
L2 <> L3

thus ( L2 is being_line & L3 is being_line & not L2 is being_point & not L3 is being_point ) by A3, A4, A8, A6, A7, Th61, Th7; :: thesis: verum

end;proof

hence
not L2 // L3
by A10, XBOOLE_0:4, EUCLIDLP:71; :: thesis: ( L2 is being_line & L3 is being_line & not L2 is being_point & not L3 is being_point )
assume A19:
L2 = L3
; :: thesis: contradiction

A20: ( A in Line (A,(the_midpoint_of_the_segment (B,C))) & the_midpoint_of_the_segment (B,C) in Line (A,(the_midpoint_of_the_segment (B,C))) & B in Line (B,(the_midpoint_of_the_segment (C,A))) & the_midpoint_of_the_segment (C,A) in Line (B,(the_midpoint_of_the_segment (C,A))) & C in Line (C,(the_midpoint_of_the_segment (A,B))) & the_midpoint_of_the_segment (A,B) in Line (C,(the_midpoint_of_the_segment (A,B))) ) by RLTOPSP1:72;

then ( B in L2 & C in L2 & B in L3 & C in L3 & rCA in L2 & rAB in L2 & rCA in L3 & rAB in L3 ) by A19, Th4;

then L2 = Line (rB,rC) by A5, A9, EUCLIDLP:30;

then A21: L2 = Line (B,C) by Th4;

( C <> the_midpoint_of_the_segment (C,A) & C in L2 & the_midpoint_of_the_segment (C,A) in LSeg (C,A) & the_midpoint_of_the_segment (C,A) in L2 & L2 is being_line ) by A3, A5, Th25, RLTOPSP1:72, A19, Th21, A6, Th61, A8;

then ( B in L2 & C in L2 & A in L2 ) by A20, Th4, Th5;

hence contradiction by A21, A5, A1, MENELAUS:13; :: thesis: verum

end;A20: ( A in Line (A,(the_midpoint_of_the_segment (B,C))) & the_midpoint_of_the_segment (B,C) in Line (A,(the_midpoint_of_the_segment (B,C))) & B in Line (B,(the_midpoint_of_the_segment (C,A))) & the_midpoint_of_the_segment (C,A) in Line (B,(the_midpoint_of_the_segment (C,A))) & C in Line (C,(the_midpoint_of_the_segment (A,B))) & the_midpoint_of_the_segment (A,B) in Line (C,(the_midpoint_of_the_segment (A,B))) ) by RLTOPSP1:72;

then ( B in L2 & C in L2 & B in L3 & C in L3 & rCA in L2 & rAB in L2 & rCA in L3 & rAB in L3 ) by A19, Th4;

then L2 = Line (rB,rC) by A5, A9, EUCLIDLP:30;

then A21: L2 = Line (B,C) by Th4;

( C <> the_midpoint_of_the_segment (C,A) & C in L2 & the_midpoint_of_the_segment (C,A) in LSeg (C,A) & the_midpoint_of_the_segment (C,A) in L2 & L2 is being_line ) by A3, A5, Th25, RLTOPSP1:72, A19, Th21, A6, Th61, A8;

then ( B in L2 & C in L2 & A in L2 ) by A20, Th4, Th5;

hence contradiction by A21, A5, A1, MENELAUS:13; :: thesis: verum

thus ( L2 is being_line & L3 is being_line & not L2 is being_point & not L3 is being_point ) by A3, A4, A8, A6, A7, Th61, Th7; :: thesis: verum

A22: L2 /\ L3 = {z} by Th16;

( D = x & D = y & D = z ) by A10, A14, A18, A22, TARSKI:def 1;

hence ex D being Point of (TOP-REAL 2) st

( (median (A,B,C)) /\ (median (B,C,A)) = {D} & (median (B,C,A)) /\ (median (C,A,B)) = {D} & (median (C,A,B)) /\ (median (A,B,C)) = {D} ) by A14, A18, A22, A8; :: thesis: verum