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);

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 )

hence
|.(C - A).| = |.(C - B).|
by Th40; :: thesis: verumthus
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;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