let A, B be Point of (TOP-REAL 2); :: thesis: the_midpoint_of_the_segment (A,B) in LSeg (A,B)

consider C being Point of (TOP-REAL 2) such that

A1: C in LSeg (A,B) and

A2: C = the_midpoint_of_the_segment (A,B) and

|.(A - C).| = half_length (A,B) by Def1;

thus the_midpoint_of_the_segment (A,B) in LSeg (A,B) by A1, A2; :: thesis: verum

consider C being Point of (TOP-REAL 2) such that

A1: C in LSeg (A,B) and

A2: C = the_midpoint_of_the_segment (A,B) and

|.(A - C).| = half_length (A,B) by Def1;

thus the_midpoint_of_the_segment (A,B) in LSeg (A,B) by A1, A2; :: thesis: verum