theorem Th23: :: PASCAL:23

for p2, p4, p5, p7, p9 being Point of (TOP-REAL 3) st |{p2,p4,p9}| = 0 holds
|{p2,p4,p5}| * |{p2,p9,p7}| = - (|{p2,p4,p7}| * |{p2,p5,p9}|)