let A, B be Point of (TOP-REAL 2); :: thesis: the_midpoint_of_the_segment (A,B) = (1 / 2) * (A + B)

now :: thesis: ( (1 / 2) * (A + B) in LSeg (A,B) & |.(A - ((1 / 2) * (A + B))).| = half_length (A,B) )

(1 / 2) * (A + B) = ((1 - (1 / 2)) * A) + ((1 / 2) * B) by RLVECT_1:def 5;
then (1 / 2) * (A + B) in { (((1 - r) * A) + (r * B)) where r is Real : ( 0 <= r & r <= 1 ) } ;
hence (1 / 2) * (A + B) in LSeg (A,B) by RLTOPSP1:def 2; :: thesis: |.(A - ((1 / 2) * (A + B))).| = half_length (A,B)
thus |.(A - ((1 / 2) * (A + B))).| = half_length (A,B) by Th18; :: thesis: verum

end;

hence the_midpoint_of_the_segment (A,B) = (1 / 2) * (A + B) by Def1; :: thesis: verum