theorem :: ANPROJ_8:102

for N being invertible Matrix of 3,F_Real
for p, q, r being Point of (ProjectiveSpace (TOP-REAL 3)) holds
( p,q,r are_collinear iff (homography N) . p,(homography N) . q,(homography N) . r are_collinear )