theorem Th37: :: BKMODEL2:48

for s being Element of (ProjectiveSpace (TOP-REAL 3))
for p, q, r being Element of absolute st p,q,r are_mutually_distinct & s in (tangent p) /\ (tangent q) holds
ex N being invertible Matrix of 3,F_Real st
( (homography N) .: absolute = absolute & (homography N) . Dir101 = p & (homography N) . Dirm101 = q & (homography N) . Dir011 = r & (homography N) . Dir010 = s )