let N be invertible Matrix of 3,F_Real; :: thesis: for p, q, r, s being Element of (ProjectiveSpace (TOP-REAL 3)) st Line (((homography N) . p),((homography N) . q)) = Line (((homography N) . r),((homography N) . s)) holds
( p,q,r are_collinear & p,q,s are_collinear & r,s,p are_collinear & r,s,q are_collinear )
let p, q, r, s be Element of (ProjectiveSpace (TOP-REAL 3)); :: thesis: ( Line (((homography N) . p),((homography N) . q)) = Line (((homography N) . r),((homography N) . s)) implies ( p,q,r are_collinear & p,q,s are_collinear & r,s,p are_collinear & r,s,q are_collinear ) )
assume A1: Line (((homography N) . p),((homography N) . q)) = Line (((homography N) . r),((homography N) . s)) ; :: thesis: ( p,q,r are_collinear & p,q,s are_collinear & r,s,p are_collinear & r,s,q are_collinear )
hence p,q,r are_collinear by ANPROJ_8:102, Th39; :: thesis: ( p,q,s are_collinear & r,s,p are_collinear & r,s,q are_collinear )
Line (((homography N) . p),((homography N) . q)) = Line (((homography N) . s),((homography N) . r)) by A1, Th40;
hence p,q,s are_collinear by ANPROJ_8:102, Th39; :: thesis: ( r,s,p are_collinear & r,s,q are_collinear )
thus r,s,p are_collinear by A1, ANPROJ_8:102, Th39; :: thesis: r,s,q are_collinear
Line (((homography N) . q),((homography N) . p)) = Line (((homography N) . r),((homography N) . s)) by A1, Th40;
hence r,s,q are_collinear by ANPROJ_8:102, Th39; :: thesis: verum