theorem Th28: :: EUCLID12:35

for A, B, C being Point of (TOP-REAL 2) st C in LSeg (A,B) & |.(A - C).| = |.(B - C).| holds
C = the_midpoint_of_the_segment (A,B)