:: deftheorem Def6 defines ProjectiveCollinearity ANPROJ_1:def 6 :
for V being non trivial RealLinearSpace
for b₂ being Relation3 of ProjectivePoints V holds
( b₂ = ProjectiveCollinearity V iff for x, y, z being object holds
( [x,y,z] in b₂ iff ex p, q, r being Element of V st
( x = Dir p & y = Dir q & z = Dir r & not p is zero & not q is zero & not r is zero & p,q,r are_LinDep ) ) );