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_{1} being Point of (TOP-REAL 2) st

( (the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) = {b_{1}} & (the_perpendicular_bisector (B,C)) /\ (the_perpendicular_bisector (C,A)) = {b_{1}} & (the_perpendicular_bisector (C,A)) /\ (the_perpendicular_bisector (A,B)) = {b_{1}} )
by A2; :: thesis: verum

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

( (the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) = {b