theorem Th21: :: PASCAL:21
for p1, p2, p5, p7, p9 being Point of (TOP-REAL 3) st |{p1,p5,p9}| = 0 holds
|{p1,p5,p7}| * |{p2,p5,p9}| = - (|{p1,p2,p5}| * |{p5,p9,p7}|)