for N being invertible Matrix of 3,F_Real
for P being Point of (ProjectiveSpace (TOP-REAL 3))
for l being LINE of (IncProjSp_of real_projective_plane) st P in (line_homography N) . l holds
(homography (N ~)) . P in l