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