let p1, p2, p3 be Point of (TOP-REAL 3); :: thesis: |{p1,p2,p3}| = |{p2,p3,p1}|
|{p1,p2,p3}| = |(|[(p1 `1),(p1 `2),(p1 `3)]|,|[(((p2 `2) * (p3 `3)) - ((p2 `3) * (p3 `2))),(((p2 `3) * (p3 `1)) - ((p2 `1) * (p3 `3))),(((p2 `1) * (p3 `2)) - ((p2 `2) * (p3 `1)))]|)| by Th3
.= (((p1 `1) * (((p2 `2) * (p3 `3)) - ((p2 `3) * (p3 `2)))) + ((p1 `2) * (((p2 `3) * (p3 `1)) - ((p2 `1) * (p3 `3))))) + ((p1 `3) * (((p2 `1) * (p3 `2)) - ((p2 `2) * (p3 `1)))) by Th30
.= (((p2 `1) * (((p3 `2) * (p1 `3)) - ((p3 `3) * (p1 `2)))) + ((p2 `2) * (((p3 `3) * (p1 `1)) - ((p3 `1) * (p1 `3))))) + ((p2 `3) * (((p3 `1) * (p1 `2)) - ((p3 `2) * (p1 `1))))
.= |(|[(p2 `1),(p2 `2),(p2 `3)]|,|[(((p3 `2) * (p1 `3)) - ((p3 `3) * (p1 `2))),(((p3 `3) * (p1 `1)) - ((p3 `1) * (p1 `3))),(((p3 `1) * (p1 `2)) - ((p3 `2) * (p1 `1)))]|)| by Th30
.= |(p2,(p3 <X> p1))| by Th3 ;
hence |{p1,p2,p3}| = |{p2,p3,p1}| ; :: thesis: verum