let A, B be Point of (TOP-REAL 2); :: thesis: ( the_midpoint_of_the_segment (A,B) = B implies A = B )

assume the_midpoint_of_the_segment (A,B) = B ; :: thesis: A = B

then the_midpoint_of_the_segment (B,A) = B by Th23;

hence A = B by Th25; :: thesis: verum

assume the_midpoint_of_the_segment (A,B) = B ; :: thesis: A = B

then the_midpoint_of_the_segment (B,A) = B by Th23;

hence A = B by Th25; :: thesis: verum