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
( (the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) = {D} & (the_perpendicular_bisector (B,C)) /\ (the_perpendicular_bisector (C,A)) = {D} & (the_perpendicular_bisector (C,A)) /\ (the_perpendicular_bisector (A,B)) = {D} & |.(D - A).| = |.(D - B).| & |.(D - A).| = |.(D - C).| & |.(D - B).| = |.(D - C).| ) )
assume A1: A,B,C is_a_triangle ; :: thesis: ex D being Point of (TOP-REAL 2) st
( (the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) = {D} & (the_perpendicular_bisector (B,C)) /\ (the_perpendicular_bisector (C,A)) = {D} & (the_perpendicular_bisector (C,A)) /\ (the_perpendicular_bisector (A,B)) = {D} & |.(D - A).| = |.(D - B).| & |.(D - A).| = |.(D - C).| & |.(D - B).| = |.(D - C).| )
then A2: A,B,C are_mutually_distinct by EUCLID_6:20;
set MAB = the_perpendicular_bisector (A,B);
set MiAB = the_midpoint_of_the_segment (A,B);
set MBC = the_perpendicular_bisector (B,C);
set MiBC = the_midpoint_of_the_segment (B,C);
set MCA = the_perpendicular_bisector (C,A);
set MiCA = the_midpoint_of_the_segment (C,A);
(the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) is being_point by A1, Th46;
then consider x being Element of REAL 2 such that
A3: (the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) = {x} ;
B,C,A is_a_triangle by A1, MENELAUS:15;
then (the_perpendicular_bisector (B,C)) /\ (the_perpendicular_bisector (C,A)) is being_point by Th46;
then consider y being Element of REAL 2 such that
A4: (the_perpendicular_bisector (B,C)) /\ (the_perpendicular_bisector (C,A)) = {y} ;
C,A,B is_a_triangle by A1, MENELAUS:15;
then (the_perpendicular_bisector (C,A)) /\ (the_perpendicular_bisector (A,B)) is being_point by Th46;
then consider z being Element of REAL 2 such that
A5: (the_perpendicular_bisector (C,A)) /\ (the_perpendicular_bisector (A,B)) = {z} ;
x in (the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) by A3, TARSKI:def 1;
then A6: ( x in the_perpendicular_bisector (A,B) & x in the_perpendicular_bisector (B,C) ) by XBOOLE_0:def 4;
reconsider Px = x as Point of (TOP-REAL 2) by EUCLID:22;
A7: ( |.(Px - A).| = |.(Px - B).| & |.(Px - B).| = |.(Px - C).| ) by A6, Th41;
y in (the_perpendicular_bisector (B,C)) /\ (the_perpendicular_bisector (C,A)) by A4, TARSKI:def 1;
then A8: ( y in the_perpendicular_bisector (B,C) & y in the_perpendicular_bisector (C,A) ) by XBOOLE_0:def 4;
reconsider Py = y as Point of (TOP-REAL 2) by EUCLID:22;
( |.(Py - B).| = |.(Py - C).| & |.(Py - C).| = |.(Py - A).| ) by A8, Th41;
then Py in the_perpendicular_bisector (A,B) by A2, Th45;
then Py in (the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) by A8, XBOOLE_0:def 4;
then A9: Py = Px by A3, TARSKI:def 1;
z in (the_perpendicular_bisector (C,A)) /\ (the_perpendicular_bisector (A,B)) by A5, TARSKI:def 1;
then A10: ( z in the_perpendicular_bisector (C,A) & z in the_perpendicular_bisector (A,B) ) by XBOOLE_0:def 4;
reconsider Pz = z as Point of (TOP-REAL 2) by EUCLID:22;
( |.(Pz - C).| = |.(Pz - A).| & |.(Pz - A).| = |.(Pz - B).| ) by A10, Th41;
then Pz in the_perpendicular_bisector (B,C) by A2, Th45;
then A11: Pz in (the_perpendicular_bisector (B,C)) /\ (the_perpendicular_bisector (C,A)) by A10, XBOOLE_0:def 4;
take Px ; :: thesis: ( (the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) = {Px} & (the_perpendicular_bisector (B,C)) /\ (the_perpendicular_bisector (C,A)) = {Px} & (the_perpendicular_bisector (C,A)) /\ (the_perpendicular_bisector (A,B)) = {Px} & |.(Px - A).| = |.(Px - B).| & |.(Px - A).| = |.(Px - C).| & |.(Px - B).| = |.(Px - C).| )
thus ( (the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) = {Px} & (the_perpendicular_bisector (B,C)) /\ (the_perpendicular_bisector (C,A)) = {Px} & (the_perpendicular_bisector (C,A)) /\ (the_perpendicular_bisector (A,B)) = {Px} & |.(Px - A).| = |.(Px - B).| & |.(Px - A).| = |.(Px - C).| & |.(Px - B).| = |.(Px - C).| ) by A7, A3, A4, A5, TARSKI:def 1, A11, A9; :: thesis: verum