theorem
for
p1,
q1,
r1,
p2,
q2,
r2 being
Element of
absolute st
p1,
q1,
r1 are_mutually_distinct &
p2,
q2,
r2 are_mutually_distinct 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 )