theorem :: EUCLID_8:84

for x1, x2, x3, y1, y2, y3 being Real holds |[x1,x2,x3]| <X> |[y1,y2,y3]| = |[((x2 * y3) - (x3 * y2)),((x3 * y1) - (x1 * y3)),((x1 * y2) - (x2 * y1))]|