theorem Th27: :: EUCLID12:34

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