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