let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A <> B & C in the_perpendicular_bisector (A,B) implies |.(C - A).| = |.(C - B).| )
assume that
A1: A <> B and
A2: C in the_perpendicular_bisector (A,B) ; :: thesis: |.(C - A).| = |.(C - B).|
consider L1, L2 being Element of line_of_REAL 2 such that
A3: the_perpendicular_bisector (A,B) = L2 and
A4: L1 = Line (A,B) and
A5: L1 _|_ L2 and
A6: L1 /\ L2 = {(the_midpoint_of_the_segment (A,B))} by A1, Def2;
set D = the_midpoint_of_the_segment (A,B);

now :: thesis: ( A <> B & L1 = Line (A,B) & the_midpoint_of_the_segment (A,B) in LSeg (A,B) & |.(A - (the_midpoint_of_the_segment (A,B))).| = (1 / 2) * |.(A - B).| & the_midpoint_of_the_segment (A,B) in L2 & L1 _|_ L2 & C in L2 )

thus A <> B by A1; :: thesis: ( L1 = Line (A,B) & the_midpoint_of_the_segment (A,B) in LSeg (A,B) & |.(A - (the_midpoint_of_the_segment (A,B))).| = (1 / 2) * |.(A - B).| & the_midpoint_of_the_segment (A,B) in L2 & L1 _|_ L2 & C in L2 )
thus L1 = Line (A,B) by A4; :: thesis: ( the_midpoint_of_the_segment (A,B) in LSeg (A,B) & |.(A - (the_midpoint_of_the_segment (A,B))).| = (1 / 2) * |.(A - B).| & the_midpoint_of_the_segment (A,B) in L2 & L1 _|_ L2 & C in L2 )
thus the_midpoint_of_the_segment (A,B) in LSeg (A,B) by Th21; :: thesis: ( |.(A - (the_midpoint_of_the_segment (A,B))).| = (1 / 2) * |.(A - B).| & the_midpoint_of_the_segment (A,B) in L2 & L1 _|_ L2 & C in L2 )
consider E being Point of (TOP-REAL 2) such that
E in LSeg (A,B) and
A7: the_midpoint_of_the_segment (A,B) = E and
A8: |.(A - E).| = half_length (A,B) by Def1;
thus |.(A - (the_midpoint_of_the_segment (A,B))).| = (1 / 2) * |.(A - B).| by A7, A8; :: thesis: ( the_midpoint_of_the_segment (A,B) in L2 & L1 _|_ L2 & C in L2 )
the_midpoint_of_the_segment (A,B) in L1 /\ L2 by A6, TARSKI:def 1;
hence the_midpoint_of_the_segment (A,B) in L2 by XBOOLE_0:def 4; :: thesis: ( L1 _|_ L2 & C in L2 )
thus L1 _|_ L2 by A5; :: thesis: C in L2
thus C in L2 by A2, A3; :: thesis: verum

end;

hence |.(C - A).| = |.(C - B).| by Th40; :: thesis: verum