let A, B, C be Point of (TOP-REAL 2); :: thesis: ( C in LSeg (A,B) & |.(A - C).| = |.(B - C).| implies C = the_midpoint_of_the_segment (A,B) )
assume that
A1: C in LSeg (A,B) and
A2: |.(A - C).| = |.(B - C).| ; :: thesis: C = the_midpoint_of_the_segment (A,B)
|.(A - C).| = half_length (A,B) by A1, A2, Th27;
hence C = the_midpoint_of_the_segment (A,B) by A1, Def1; :: thesis: verum