theorem :: EUCLID13:23

for A, B, C being Point of (TOP-REAL 2) st A <> B & A <> C holds
|.(A - B).| + |.(A - C).| <> 0