theorem Th18: :: EUCLID12:25

for A, B being Point of (TOP-REAL 2) holds |.(A - ((1 / 2) * (A + B))).| = (1 / 2) * |.(A - B).|