let p1, p2, p3 be Element of REAL 3; |{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 Th1
.=
(((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 EUCLID_5:30
.=
(((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 EUCLID_5:30
.=
|(p2,(p3 <X> p1))|
by Th1
;
hence
|{p1,p2,p3}| = |{p2,p3,p1}|
; verum