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