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