<e1> <X> <e3> = |[((0 * 1) - (0 * 0)),((0 * 0) - (1 * 1)),((1 * 0) - (0 * 0))]|
.= |[((- 1) * (<e2> . 1)),((- 1) * (<e2> . 2)),((- 1) * (<e2> . 3))]|
.= - <e2> by Lm1 ;
hence <e1> <X> <e3> = - <e2> ; :: thesis: verum