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

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