theorem Th30: :: EUCLID12:38

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