theorem Th42: :: EUCLID12:57

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