let p1, p2 be Element of REAL 3; :: thesis: |{p1,p1,p2}| = 0
A1: (p1 <X> p2) . 1 = ((p1 . 2) * (p2 . 3)) - ((p1 . 3) * (p2 . 2)) ;
A2: (p1 <X> p2) . 2 = ((p1 . 3) * (p2 . 1)) - ((p1 . 1) * (p2 . 3)) ;
(p1 <X> p2) . 3 = ((p1 . 1) * (p2 . 2)) - ((p1 . 2) * (p2 . 1)) ;
then |{p1,p1,p2}| = (((p1 . 1) * (((p1 . 2) * (p2 . 3)) - ((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 A2, A1, Lm5
.= 0 ;
hence |{p1,p1,p2}| = 0 ; :: thesis: verum