theorem Th38: :: BKMODEL2:49

for p1, q1, r1, p2, q2, r2 being Element of absolute
for s1, s2 being Element of real_projective_plane st p1,q1,r1 are_mutually_distinct & p2,q2,r2 are_mutually_distinct & s1 in (tangent p1) /\ (tangent q1) & s2 in (tangent p2) /\ (tangent q2) holds
ex N being invertible Matrix of 3,F_Real st
( (homography N) .: absolute = absolute & (homography N) . p1 = p2 & (homography N) . q1 = q2 & (homography N) . r1 = r2 & (homography N) . s1 = s2 )