let A, B be Point of (TOP-REAL 2); :: thesis: ( the_midpoint_of_the_segment (A,B) = A implies A = B )
assume the_midpoint_of_the_segment (A,B) = A ; :: thesis: A = B
then A1: A = (1 / 2) * (A + B) by Th22
.= ((1 / 2) * A) + ((1 / 2) * B) by RVSUM_1:51 ;
A2: ((1 / 2) * A) + ((1 / 2) * A) = ((1 / 2) + (1 / 2)) * A by RVSUM_1:50
.= A by RVSUM_1:52 ;
reconsider rA = A, rB = B as Element of REAL 2 by EUCLID:22;
((1 / 2) * rA) + ((1 / 2) * rA) = ((1 / 2) * rA) + ((1 / 2) * rB) by A1, A2;
then 2 * ((1 / 2) * A) = 2 * ((1 / 2) * B) by RVSUM_1:25;
then ((2 * 1) / 2) * A = 2 * ((1 / 2) * B) by RVSUM_1:49;
then 1 * A = 1 * B by RVSUM_1:49;
then A = 1 * B by RVSUM_1:52;
hence A = B by RVSUM_1:52; :: thesis: verum