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