let p1, p2, p3 be Element of REAL 3; p1 <X> (p2 <X> p3) = (|(p1,p3)| * p2) - (|(p1,p2)| * p3)
A1:
p2 = |[(p2 . 1),(p2 . 2),(p2 . 3)]|
by Lm1;
A2:
p3 = |[(p3 . 1),(p3 . 2),(p3 . 3)]|
by Lm1;
A3:
p1 <X> (p2 <X> p3) = |[(p1 . 1),(p1 . 2),(p1 . 3)]| <X> |[(((p2 . 2) * (p3 . 3)) - ((p2 . 3) * (p3 . 2))),(((p2 . 3) * (p3 . 1)) - ((p2 . 1) * (p3 . 3))),(((p2 . 1) * (p3 . 2)) - ((p2 . 2) * (p3 . 1)))]|
by Lm1;
A4:
p1 <X> (p2 <X> p3) = |[(((p1 . 2) * (((p2 . 1) * (p3 . 2)) - ((p2 . 2) * (p3 . 1)))) - ((p1 . 3) * (((p2 . 3) * (p3 . 1)) - ((p2 . 1) * (p3 . 3))))),(((p1 . 3) * (((p2 . 2) * (p3 . 3)) - ((p2 . 3) * (p3 . 2)))) - ((p1 . 1) * (((p2 . 1) * (p3 . 2)) - ((p2 . 2) * (p3 . 1))))),(((p1 . 1) * (((p2 . 3) * (p3 . 1)) - ((p2 . 1) * (p3 . 3)))) - ((p1 . 2) * (((p2 . 2) * (p3 . 3)) - ((p2 . 3) * (p3 . 2)))))]|
by A3, Th129;
A5:
p1 <X> (p2 <X> p3) = |[((((((p1 . 2) * (p3 . 2)) + ((p1 . 3) * (p3 . 3))) + ((p1 . 1) * (p3 . 1))) * (p2 . 1)) - (((((p1 . 2) * (p2 . 2)) + ((p1 . 3) * (p2 . 3))) + ((p1 . 1) * (p2 . 1))) * (p3 . 1))),((((((p1 . 3) * (p3 . 3)) + ((p1 . 1) * (p3 . 1))) + ((p1 . 2) * (p3 . 2))) * (p2 . 2)) - (((((p1 . 3) * (p2 . 3)) + ((p1 . 1) * (p2 . 1))) + ((p1 . 2) * (p2 . 2))) * (p3 . 2))),((((((p1 . 1) * (p3 . 1)) + ((p1 . 2) * (p3 . 2))) + ((p1 . 3) * (p3 . 3))) * (p2 . 3)) - (((((p1 . 1) * (p2 . 1)) + ((p1 . 2) * (p2 . 2))) + ((p1 . 3) * (p2 . 3))) * (p3 . 3)))]|
by A4;
A6:
|(p1,p3)| = (((p1 . 1) * (p3 . 1)) + ((p1 . 2) * (p3 . 2))) + ((p1 . 3) * (p3 . 3))
by Lm8;
A7:
p1 <X> (p2 <X> p3) = |[(|(p1,p3)| * (p2 . 1)),(|(p1,p3)| * (p2 . 2)),(|(p1,p3)| * (p2 . 3))]| - |[(((((p1 . 1) * (p2 . 1)) + ((p1 . 2) * (p2 . 2))) + ((p1 . 3) * (p2 . 3))) * (p3 . 1)),(((((p1 . 1) * (p2 . 1)) + ((p1 . 2) * (p2 . 2))) + ((p1 . 3) * (p2 . 3))) * (p3 . 2)),(((((p1 . 1) * (p2 . 1)) + ((p1 . 2) * (p2 . 2))) + ((p1 . 3) * (p2 . 3))) * (p3 . 3))]|
by A5, A6, LmA63;
A8:
|(p1,p2)| = (((p1 . 1) * (p2 . 1)) + ((p1 . 2) * (p2 . 2))) + ((p1 . 3) * (p2 . 3))
by Lm8;
p1 <X> (p2 <X> p3) = (|(p1,p3)| * |[(p2 . 1),(p2 . 2),(p2 . 3)]|) - |[(|(p1,p2)| * (p3 . 1)),(|(p1,p2)| * (p3 . 2)),(|(p1,p2)| * (p3 . 3))]|
by A7, A8, Th9;
hence
p1 <X> (p2 <X> p3) = (|(p1,p3)| * p2) - (|(p1,p2)| * p3)
by A1, A2, Th9; verum