consider D being Point of (TOP-REAL 2) such that
A2: ( (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} ) and
( |.(D - A).| = |.(D - B).| & |.(D - A).| = |.(D - C).| & |.(D - B).| = |.(D - C).| ) by A1, Th47;
thus ex b₁ being Point of (TOP-REAL 2) st
( (the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) = {b₁} & (the_perpendicular_bisector (B,C)) /\ (the_perpendicular_bisector (C,A)) = {b₁} & (the_perpendicular_bisector (C,A)) /\ (the_perpendicular_bisector (A,B)) = {b₁} ) by A2; :: thesis: verum