let A, B, C be Point of (TOP-REAL 2); ( 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
; (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 ( not LAB2 // LBC2 & LAB2 is being_line & LBC2 is being_line )hereby ( LAB2 is being_line & LBC2 is being_line )
assume
LAB2 // LBC2
;
contradictionthen
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;
verum
end; thus
LAB2 is
being_line
by A5, EUCLIDLP:67;
LBC2 is being_line thus
LBC2 is
being_line
by A8, EUCLIDLP:67;
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; verum