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;

hence (the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) is being_point by A3, A6, Th16; :: thesis: verum

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 )

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;hereby :: thesis: ( LAB2 is being_line & LBC2 is being_line )

thus
LAB2 is being_line
by A5, EUCLIDLP:67; :: thesis: 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;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

thus LBC2 is being_line by A8, EUCLIDLP:67; :: thesis: verum

hence (the_perpendicular_bisector (A,B)) /\ (the_perpendicular_bisector (B,C)) is being_point by A3, A6, Th16; :: thesis: verum