let p3, p4, p5, p6, p8 be Point of (TOP-REAL 3); ( |{p3,p4,p8}| = 0 implies |{p3,p4,p6}| * |{p3,p5,p8}| = |{p3,p4,p5}| * |{p3,p6,p8}| )
assume A1:
|{p3,p4,p8}| = 0
; |{p3,p4,p6}| * |{p3,p5,p8}| = |{p3,p4,p5}| * |{p3,p6,p8}|
((|{p3,p4,p6}| * |{p3,p5,p8}|) - (|{p3,p4,p5}| * |{p3,p6,p8}|)) + (|{p3,p4,p8}| * |{p3,p6,p5}|) = 0
by ANPROJ_8:28;
hence
|{p3,p4,p6}| * |{p3,p5,p8}| = |{p3,p4,p5}| * |{p3,p6,p8}|
by A1; verum