let p1, p2 be Point of (TOP-REAL 3); :: thesis: ( |{p1,p1,p2}| = 0 & |{p2,p1,p2}| = 0 )
A1: |{p1,p1,p2}| = (((p1 `1 ) * ((p1 <X> p2) `1 )) + ((p1 `2 ) * ((p1 <X> p2) `2 ))) + ((p1 `3 ) * ((p1 <X> p2) `3 )) by Th29
.= (((p1 `1 ) * (((p1 `2 ) * (p2 `3 )) - ((p1 `3 ) * (p2 `2 )))) + ((p1 `2 ) * ((p1 <X> p2) `2 ))) + ((p1 `3 ) * ((p1 <X> p2) `3 )) by FINSEQ_1:62
.= (((p1 `1 ) * (((p1 `2 ) * (p2 `3 )) - ((p1 `3 ) * (p2 `2 )))) + ((p1 `2 ) * (((p1 `3 ) * (p2 `1 )) - ((p1 `1 ) * (p2 `3 ))))) + ((p1 `3 ) * ((p1 <X> p2) `3 )) by FINSEQ_1:62
.= ((((p1 `1 ) * ((p1 `2 ) * (p2 `3 ))) - ((p1 `1 ) * ((p1 `3 ) * (p2 `2 )))) + ((p1 `2 ) * (((p1 `3 ) * (p2 `1 )) - ((p1 `1 ) * (p2 `3 ))))) + ((p1 `3 ) * (((p1 `1 ) * (p2 `2 )) - ((p1 `2 ) * (p2 `1 )))) by FINSEQ_1:62
.= 0 ;
|{p2,p1,p2}| = (((p2 `1 ) * ((p1 <X> p2) `1 )) + ((p2 `2 ) * ((p1 <X> p2) `2 ))) + ((p2 `3 ) * ((p1 <X> p2) `3 )) by Th29
.= (((p2 `1 ) * (((p1 `2 ) * (p2 `3 )) - ((p1 `3 ) * (p2 `2 )))) + ((p2 `2 ) * ((p1 <X> p2) `2 ))) + ((p2 `3 ) * ((p1 <X> p2) `3 )) by FINSEQ_1:62
.= (((p2 `1 ) * (((p1 `2 ) * (p2 `3 )) - ((p1 `3 ) * (p2 `2 )))) + ((p2 `2 ) * (((p1 `3 ) * (p2 `1 )) - ((p1 `1 ) * (p2 `3 ))))) + ((p2 `3 ) * ((p1 <X> p2) `3 )) by FINSEQ_1:62
.= ((((p2 `1 ) * ((p1 `2 ) * (p2 `3 ))) - ((p2 `1 ) * ((p1 `3 ) * (p2 `2 )))) + ((p2 `2 ) * (((p1 `3 ) * (p2 `1 )) - ((p1 `1 ) * (p2 `3 ))))) + ((p2 `3 ) * (((p1 `1 ) * (p2 `2 )) - ((p1 `2 ) * (p2 `1 )))) by FINSEQ_1:62
.= (0 - ((p2 `2 ) * ((p1 `1 ) * (p2 `3 )))) + ((p2 `2 ) * ((p1 `1 ) * (p2 `3 ))) ;
hence ( |{p1,p1,p2}| = 0 & |{p2,p1,p2}| = 0 ) by A1; :: thesis: verum