theorem Th2: :: PAPPUS:2

for P1, P4, P5 being Element of (ProjectiveSpace (TOP-REAL 3))
for p1, p2, p3, p4, p5 being Element of (TOP-REAL 3) st not p1 is zero & P1 = Dir p1 & not p4 is zero & P4 = Dir p4 & not p5 is zero & P5 = Dir p5 & P1,P4,P5 are_collinear holds
|{p1,p2,p4}| * |{p1,p3,p5}| = |{p1,p2,p5}| * |{p1,p3,p4}|