let p1, p2, p5, p7, p9 be Point of (TOP-REAL 3); :: thesis: ( |{p1,p5,p9}| = 0 implies |{p1,p5,p7}| * |{p2,p5,p9}| = - (|{p1,p2,p5}| * |{p5,p9,p7}|) )
assume A1: |{p1,p5,p9}| = 0 ; :: thesis: |{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; :: thesis: verum