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