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 Th1;
A2:
p3 = |[(p3 . 1),(p3 . 2),(p3 . 3)]|
by Th1;
A3:
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)))]|
;
|(p1,p3)| = (((p1 . 1) * (p3 . 1)) + ((p1 . 2) * (p3 . 2))) + ((p1 . 3) * (p3 . 3))
by Lm5;
then A4:
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 A3, Lm11;
|(p1,p2)| = (((p1 . 1) * (p2 . 1)) + ((p1 . 2) * (p2 . 2))) + ((p1 . 3) * (p2 . 3))
by Lm5;
then
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 A4, Th50;
hence
p1 <X> (p2 <X> p3) = (|(p1,p3)| * p2) - (|(p1,p2)| * p3)
by A1, A2, Th50; verum