let p1, p2, p3 be Point of (TOP-REAL 3); p1 <X> (p2 <X> p3) = (|(p1,p3)| * p2) - (|(p1,p2)| * p3)
A1:
( ((p1 `2) * (((p2 `1) * (p3 `2)) - ((p2 `2) * (p3 `1)))) - ((p1 `3) * (((p2 `3) * (p3 `1)) - ((p2 `1) * (p3 `3)))) = (((((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) * (((p2 `2) * (p3 `3)) - ((p2 `3) * (p3 `2)))) - ((p1 `1) * (((p2 `1) * (p3 `2)) - ((p2 `2) * (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)) )
;
A2:
((p1 `1) * (((p2 `3) * (p3 `1)) - ((p2 `1) * (p3 `3)))) - ((p1 `2) * (((p2 `2) * (p3 `3)) - ((p2 `3) * (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 <X> (p2 <X> p3) =
|[(((((p1 `1) * (p3 `1)) + ((p1 `2) * (p3 `2))) + ((p1 `3) * (p3 `3))) * (p2 `1)),(((((p1 `1) * (p3 `1)) + ((p1 `2) * (p3 `2))) + ((p1 `3) * (p3 `3))) * (p2 `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 `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 A1, A2, Th13
.=
(((((p1 `1) * (p3 `1)) + ((p1 `2) * (p3 `2))) + ((p1 `3) * (p3 `3))) * |[(p2 `1),(p2 `2),(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 Th8
.=
(((((p1 `1) * (p3 `1)) + ((p1 `2) * (p3 `2))) + ((p1 `3) * (p3 `3))) * |[(p2 `1),(p2 `2),(p2 `3)]|) - (((((p1 `1) * (p2 `1)) + ((p1 `2) * (p2 `2))) + ((p1 `3) * (p2 `3))) * |[(p3 `1),(p3 `2),(p3 `3)]|)
by Th8
.=
(|(p1,p3)| * |[(p2 `1),(p2 `2),(p2 `3)]|) - (((((p1 `1) * (p2 `1)) + ((p1 `2) * (p2 `2))) + ((p1 `3) * (p2 `3))) * |[(p3 `1),(p3 `2),(p3 `3)]|)
by Th29
.=
(|(p1,p3)| * |[(p2 `1),(p2 `2),(p2 `3)]|) - (|(p1,p2)| * |[(p3 `1),(p3 `2),(p3 `3)]|)
by Th29
.=
(|(p1,p3)| * p2) - (|(p1,p2)| * |[(p3 `1),(p3 `2),(p3 `3)]|)
by Th3
;
hence
p1 <X> (p2 <X> p3) = (|(p1,p3)| * p2) - (|(p1,p2)| * p3)
by Th3; verum