theorem :: ANPROJ_8:11

for V being non trivial RealLinearSpace
for p, q, r being Element of (ProjectiveSpace V) holds
( p,q,r are_collinear iff ex u, v, w being Element of V st
( p = Dir u & q = Dir v & r = Dir w & not u is zero & not v is zero & not w is zero & ex a, b, c being Real st
( ((a * u) + (b * v)) + (c * w) = 0. V & ( a <> 0 or b <> 0 or c <> 0 ) ) ) )