let p1, p2 be Element of REAL 3; :: thesis: |{p1,p2,p2}| = 0
|{p1,p2,p2}| = (((p1 . 1) * ((p2 <X> p2) . 1)) + ((p1 . 2) * ((p2 <X> p2) . 2))) + ((p1 . 3) * ((p2 <X> p2) . 3)) by Lm5
.= (((p1 . 1) * (((p2 . 2) * (p2 . 3)) - ((p2 . 3) * (p2 . 2)))) + ((p1 . 2) * ((p2 <X> p2) . 2))) + ((p1 . 3) * ((p2 <X> p2) . 3))
.= (((p1 . 1) * (((p2 . 2) * (p2 . 3)) - ((p2 . 3) * (p2 . 2)))) + ((p1 . 2) * (((p2 . 3) * (p2 . 1)) - ((p2 . 1) * (p2 . 3))))) + ((p1 . 3) * ((p2 <X> p2) . 3))
.= ((((p1 . 1) * ((p2 . 2) * (p2 . 3))) - ((p1 . 1) * ((p2 . 3) * (p2 . 2)))) + ((p1 . 2) * (((p2 . 3) * (p2 . 1)) - ((p2 . 1) * (p2 . 3))))) + ((p1 . 3) * (((p2 . 1) * (p2 . 2)) - ((p2 . 2) * (p2 . 1))))
.= (0 - ((p2 . 2) * ((p2 . 1) * (p2 . 3)))) + ((p2 . 2) * ((p2 . 1) * (p2 . 3))) ;
hence |{p1,p2,p2}| = 0 ; :: thesis: verum