let p1, p2, p3 be Point of (TOP-REAL 3); :: thesis: |{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)| ; :: thesis: verum