theorem Th24: :: EUCLID12:31

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