let P1, P4, P5 be Element of (ProjectiveSpace (TOP-REAL 3)); :: thesis: 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}|
let p1, p2, p3, p4, p5 be Element of (TOP-REAL 3); :: thesis: ( 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 implies |{p1,p2,p4}| * |{p1,p3,p5}| = |{p1,p2,p5}| * |{p1,p3,p4}| )
assume that
A1: ( not p1 is zero & P1 = Dir p1 ) and
A2: ( not p4 is zero & P4 = Dir p4 ) and
A3: ( not p5 is zero & P5 = Dir p5 ) and
A4: P1,P4,P5 are_collinear ; :: thesis: |{p1,p2,p4}| * |{p1,p3,p5}| = |{p1,p2,p5}| * |{p1,p3,p4}|
A5: ((|{p1,p2,p3}| * |{p1,p4,p5}|) - (|{p1,p2,p4}| * |{p1,p3,p5}|)) + (|{p1,p2,p5}| * |{p1,p3,p4}|) = 0 by ANPROJ_8:28;
|{p1,p4,p5}| = 0 by A1, A2, A3, A4, BKMODEL1:1;
hence |{p1,p2,p4}| * |{p1,p3,p5}| = |{p1,p2,p5}| * |{p1,p3,p4}| by A5; :: thesis: verum