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;
now :: thesis: ( not L1 // L2 & L1 is being_line & L2 is being_line & not L1 is being_point & not L2 is being_point )
L1 <> L2
proof
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;
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 )
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;
then consider x being Element of REAL 2 such that
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 )
L1 <> L3
proof
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;
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 )
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;
then consider y being Element of REAL 2 such that
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 )
L2 <> L3
proof
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;
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 )
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;
then consider z being Element of REAL 2 such that
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