let p2, p4, p6, p7, p8 be Point of (TOP-REAL 3); :: thesis: ( |{p2,p6,p7}| = 0 implies |{p2,p4,p7}| * |{p2,p6,p8}| = - (|{p2,p4,p6}| * |{p2,p8,p7}|) )
assume A1: |{p2,p6,p7}| = 0 ; :: thesis: |{p2,p4,p7}| * |{p2,p6,p8}| = - (|{p2,p4,p6}| * |{p2,p8,p7}|)
A2: ( |{p2,p7,p6}| = - |{p2,p6,p7}| & |{p2,p7,p8}| = - |{p2,p8,p7}| ) by ANPROJ_8:29;
((|{p2,p4,p7}| * |{p2,p6,p8}|) - (|{p2,p4,p6}| * |{p2,p7,p8}|)) + (|{p2,p4,p8}| * |{p2,p7,p6}|) = 0 by ANPROJ_8:28;
hence |{p2,p4,p7}| * |{p2,p6,p8}| = - (|{p2,p4,p6}| * |{p2,p8,p7}|) by A1, A2; :: thesis: verum