theorem :: EUCLID_5:34

for p1, p2, p3 being Point of (TOP-REAL 3) holds |{p1,p2,p3}| = |{p3,p1,p2}| by Th33;