let p1, p2, p5, p7, p9 be Point of (TOP-REAL 3); ( |{p1,p5,p9}| = 0 implies |{p1,p5,p7}| * |{p2,p5,p9}| = - (|{p1,p2,p5}| * |{p5,p9,p7}|) )
assume A1:
|{p1,p5,p9}| = 0
; |{p1,p5,p7}| * |{p2,p5,p9}| = - (|{p1,p2,p5}| * |{p5,p9,p7}|)
A2:
( |{p1,p2,p5}| = |{p5,p1,p2}| & |{p1,p5,p9}| = - |{p5,p1,p9}| & |{p5,p1,p7}| = - |{p1,p5,p7}| & |{p5,p2,p9}| = - |{p2,p5,p9}| & |{p5,p9,p7}| = - |{p5,p7,p9}| )
by ANPROJ_8:29, ANPROJ_8:30, Th01;
then A3:
|{p5,p1,p9}| = 0
by A1;
((|{p5,p1,p7}| * |{p5,p2,p9}|) - (|{p5,p1,p2}| * |{p5,p7,p9}|)) + (|{p5,p1,p9}| * |{p5,p7,p2}|) = 0
by ANPROJ_8:28;
hence
|{p1,p5,p7}| * |{p2,p5,p9}| = - (|{p1,p2,p5}| * |{p5,p9,p7}|)
by A2, A3; verum