theorem Th20: :: ANPROJ_9:24

for P1, P2, P3 being Point of (ProjectiveSpace (TOP-REAL 3)) st not P1,P2,P3 are_collinear holds
ex N being invertible Matrix of 3,F_Real st
( (homography N) . P1 = Dir100 & (homography N) . P2 = Dir010 & (homography N) . P3 = Dir001 )