theorem Th23: :: EUCLID12:30

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