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