theorem :: BKMODEL1:69

for N being invertible Matrix of 3,F_Real
for P, Q, R being Point of (ProjectiveSpace (TOP-REAL 3)) st P <> Q & (homography N) . P = Q & (homography N) . Q = P & P,Q,R are_collinear holds
(homography N) . ((homography N) . R) = R