theorem Th19: :: BKMODEL3:23

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 (homography N) . P in l holds
P in (line_homography (N ~)) . l