let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle implies (the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) is being_point )
assume A1: A,B,C is_a_triangle ; :: thesis: (the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) is being_point
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);
consider LAB1, LAB2 being Element of line_of_REAL 2 such that
A3: the_perpendicular_bisector (A,B) = LAB2 and
A4: LAB1 = Line (A,B) and
A5: LAB1 _|_ LAB2 and
LAB1 /\ LAB2 = {(the_midpoint_of_the_segment (A,B))} by A2, Def2;
consider LBC1, LBC2 being Element of line_of_REAL 2 such that
A6: the_perpendicular_bisector (B,C) = LBC2 and
A7: LBC1 = Line (B,C) and
A8: LBC1 _|_ LBC2 and
LBC1 /\ LBC2 = {(the_midpoint_of_the_segment (B,C))} by A2, Def2;
now :: thesis: ( not LAB2 // LBC2 & LAB2 is being_line & LBC2 is being_line )
hereby :: thesis: ( LAB2 is being_line & LBC2 is being_line )
assume LAB2 // LBC2 ; :: thesis: contradiction
then LBC1 _|_ LAB2 by A8, EUCLIDLP:61;
then A9: LAB1 // LBC1 by A5, Th13, EUCLIDLP:111;
( B in LAB1 & B in LBC1 ) by A4, A7, RLTOPSP1:72;
then LAB1 = LBC1 by A9, EUCLIDLP:71, XBOOLE_0:3;
then C in LAB1 by A7, RLTOPSP1:72;
then C,A,B are_collinear by A2, A4, MENELAUS:13;
hence contradiction by A1, MENELAUS:15; :: thesis: verum
end;
thus LAB2 is being_line by A5, EUCLIDLP:67; :: thesis: LBC2 is being_line
thus LBC2 is being_line by A8, EUCLIDLP:67; :: thesis: verum
end;
then ( not LAB2 // LBC2 & not LAB2 is being_point & not LBC2 is being_point ) by Th7;
hence (the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) is being_point by A3, A6, Th16; :: thesis: verum