theorem Th25: :: EUCLID12:32

for A, B being Point of (TOP-REAL 2) st the_midpoint_of_the_segment (A,B) = A holds
A = B