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