theorem Th25: :: ANPROJ_9:29

for P being Point of (ProjectiveSpace (TOP-REAL 3)) st not Dir100 , Dir010 ,P are_collinear & not Dir100 , Dir001 ,P are_collinear & not Dir010 , Dir001 ,P are_collinear holds
ex a, b, c being non zero Element of F_Real st
for N being invertible Matrix of 3,F_Real st N = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> holds
(homography N) . P = Dir111