let A, B, C be Point of (TOP-REAL 2); ( 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)
; |.(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 ( 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;
( 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;
( 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;
( |.(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;
( 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;
( L1 _|_ L2 & C in L2 )thus
L1 _|_ L2
by A5;
C in L2thus
C in L2
by A2, A3;
verum end;
hence
|.(C - A).| = |.(C - B).|
by Th40; verum