theorem :: EUCLID_8:92

for p1, p2 being Element of REAL 3 holds |{p1,p2,p2}| = 0