theorem :: EUCLID_8:91

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