theorem Th20: :: EUCLID12:27

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