for N being invertible Matrix of 3,F_Real
for p, q, r, s being Element of (ProjectiveSpace (TOP-REAL 3)) st Line (((homography N) . p),((homography N) . q)) = Line (((homography N) . r),((homography N) . s)) holds
( p,q,r are_collinear & p,q,s are_collinear & r,s,p are_collinear & r,s,q are_collinear )