let x1, x2, x3, y1, y2, y3 be Real; :: thesis: |[x1,x2,x3]| <X> |[y1,y2,y3]| = |[((x2 * y3) - (x3 * y2)),((x3 * y1) - (x1 * y3)),((x1 * y2) - (x2 * y1))]|
set p1 = |[x1,x2,x3]|;
set p2 = |[y1,y2,y3]|;
thus |[x1,x2,x3]| <X> |[y1,y2,y3]| = |[((x2 * y3) - (x3 * y2)),((x3 * y1) - (x1 * y3)),((x1 * y2) - (x2 * y1))]| ; :: thesis: verum