theorem Th9: :: EUCLID12:11

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