theorem :: BKMODEL2:57

for p, q, r, s being Element of absolute st p,q,r are_mutually_distinct & q,p,s are_mutually_distinct holds
ex N being invertible Matrix of 3,F_Real st
( (homography N) .: absolute = absolute & (homography N) . p = q & (homography N) . q = p & (homography N) . r = s & ( for t being Element of real_projective_plane st t in (tangent p) /\ (tangent q) holds
(homography N) . t = t ) )