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

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