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