let x1, y1, z1, x2, y2, z2 be Real; :: thesis: |[x1,y1,z1]| <X> |[x2,y2,z2]| = |[((y1 * z2) - (z1 * y2)),((z1 * x2) - (x1 * z2)),((x1 * y2) - (y1 * x2))]|
consider p1 being Point of (TOP-REAL 3) such that
A1: p1 = |[x1,y1,z1]| ;
A2: p1 `3 = z1 by A1, FINSEQ_1:45;
consider p2 being Point of (TOP-REAL 3) such that
A3: p2 = |[x2,y2,z2]| ;
A4: p2 `3 = z2 by A3, FINSEQ_1:45;
A5: ( p2 `1 = x2 & p2 `2 = y2 ) by A3, FINSEQ_1:45;
( p1 `1 = x1 & p1 `2 = y1 ) by A1, FINSEQ_1:45;
hence |[x1,y1,z1]| <X> |[x2,y2,z2]| = |[((y1 * z2) - (z1 * y2)),((z1 * x2) - (x1 * z2)),((x1 * y2) - (y1 * x2))]| by A1, A2, A3, A5, A4; :: thesis: verum