let A, B, C be Point of (TOP-REAL 2); ( 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).|
; 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; verum