let N be invertible Matrix of 3,F_Real; :: thesis: 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
let p, q, r, s, t, u, np, nq, nr, ns be Element of real_projective_plane; :: thesis: ( 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 implies u = (homography N) . t )
assume that
A1: ( 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 ) and
A2: not p,q,r are_collinear ; :: thesis: u = (homography N) . t
( u = (homography N) . t or Line (np,nq) = Line (nr,ns) ) by A1, Th42;
hence u = (homography N) . t by A1, A2, Th41; :: thesis: verum