let A, B be Point of (TOP-REAL 2); |.(A - (the_midpoint_of_the_segment (A,B))).| = |.((the_midpoint_of_the_segment (A,B)) - B).|
A1: |.(A - (the_midpoint_of_the_segment (A,B))).| =
|.(A - ((1 / 2) * (A + B))).|
by Th22
.=
(1 / 2) * |.(A - B).|
by Th18
;
|.((the_midpoint_of_the_segment (A,B)) - B).| =
|.(((1 / 2) * (A + B)) - B).|
by Th22
.=
|.(B - ((1 / 2) * (A + B))).|
by EUCLID_6:43
.=
(1 / 2) * |.(B - A).|
by Th18
.=
(1 / 2) * |.(A - B).|
by EUCLID_6:43
;
hence
|.(A - (the_midpoint_of_the_segment (A,B))).| = |.((the_midpoint_of_the_segment (A,B)) - B).|
by A1; verum