theorem :: EUCLID_6:42

for p1, p2 being Point of (TOP-REAL 2) holds
( |.(p1 - p2).| = 0 iff p1 = p2 ) by Lm1;