theorem :: EUCLID_5:31

for p1, p2 being Point of (TOP-REAL 3) holds
( |{p1,p1,p2}| = 0 & |{p2,p1,p2}| = 0 )