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

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; :: thesis: verum