theorem Th8: :: EUCLID12:10

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