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

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