theorem Th25: :: PASCAL:25

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