theorem Th43:
for
N being
invertible Matrix of 3,
F_Real for
p,
q,
r,
s,
t,
u,
np,
nq,
nr,
ns being
Element of
real_projective_plane st
p <> q &
r <> s &
np <> nq &
nr <> ns &
p,
q,
t are_collinear &
r,
s,
t are_collinear &
np = (homography N) . p &
nq = (homography N) . q &
nr = (homography N) . r &
ns = (homography N) . s &
np,
nq,
u are_collinear &
nr,
ns,
u are_collinear & not
p,
q,
r are_collinear holds
u = (homography N) . t