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