theorem Th26: :: PASCAL:26

for p1, p3, p5, p7, p8 being Point of (TOP-REAL 3) st |{p3,p5,p7}| = 0 holds
|{p1,p3,p5}| * |{p5,p8,p7}| = - (|{p1,p5,p7}| * |{p3,p5,p8}|)