theorem Th84: :: EUCLID_8:93
for p1, p2, p3 being Element of REAL 3 holds |{p1,p2,p3}| = |{p2,p3,p1}|