for N being invertible Matrix of 3,F_Real
for l being Element of the Lines of (IncProjSp_of real_projective_plane) holds
( (line_homography N) . ((line_homography (N ~)) . l) = l & (line_homography (N ~)) . ((line_homography N) . l) = l )