theorem Th22: :: PASCAL:22

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