theorem Th26:
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 )