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 ),(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 Th3
.=
|[(((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 Th15
;
then 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