for N being invertible Matrix of 3,F_Real
for l1, l2 being Element of the Lines of (IncProjSp_of real_projective_plane) st (line_homography N) . l1 = (line_homography N) . l2 holds
l1 = l2