for P1, P2, P3, P4 being Point of (ProjectiveSpace (TOP-REAL 3)) st not P1,P2,P3 are_collinear & not P1,P2,P4 are_collinear & not P1,P3,P4 are_collinear & not P2,P3,P4 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 & (homography N) . P4 = Dir111 )