theorem Th42:
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
u = (homography N) . t holds
Line (
np,
nq)
= Line (
nr,
ns)