let p2, p4, p5, p7, p9 be Point of (TOP-REAL 3); ( |{p2,p4,p9}| = 0 implies |{p2,p4,p5}| * |{p2,p9,p7}| = - (|{p2,p4,p7}| * |{p2,p5,p9}|) )
assume A1:
|{p2,p4,p9}| = 0
; |{p2,p4,p5}| * |{p2,p9,p7}| = - (|{p2,p4,p7}| * |{p2,p5,p9}|)
((|{p2,p4,p5}| * |{p2,p9,p7}|) - (|{p2,p4,p9}| * |{p2,p5,p7}|)) + (|{p2,p4,p7}| * |{p2,p5,p9}|) = 0
by ANPROJ_8:28;
hence
|{p2,p4,p5}| * |{p2,p9,p7}| = - (|{p2,p4,p7}| * |{p2,p5,p9}|)
by A1; verum