theorem
for
P1,
P2,
P3,
P4,
Q1,
Q2,
Q3,
Q4 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 & not
Q1,
Q2,
Q3 are_collinear & not
Q1,
Q2,
Q4 are_collinear & not
Q1,
Q3,
Q4 are_collinear & not
Q2,
Q3,
Q4 are_collinear holds
ex
N being
invertible Matrix of 3,
F_Real st
(
(homography N) . P1 = Q1 &
(homography N) . P2 = Q2 &
(homography N) . P3 = Q3 &
(homography N) . P4 = Q4 )