let V be non trivial RealLinearSpace; :: thesis: for p, q, r being Element of (ProjectiveSpace V) holds
( p,q,r is_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 & u,v,w are_LinDep ) )
let p, q, r be Element of (ProjectiveSpace V); :: thesis: ( p,q,r is_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 & u,v,w are_LinDep ) )

A1: now

assume p,q,r is_collinear ; :: thesis: 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 & u,v,w are_LinDep )
then [p,q,r] in the Collinearity of (ProjectiveSpace V) by COLLSP:def 2;
then consider u, v, w being Element of V such that
A2: ( p = Dir u & q = Dir v & r = Dir w & not u is zero & not v is zero & not w is zero & u,v,w are_LinDep ) by ANPROJ_1:24;
take u = u; :: thesis: ex 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 & u,v,w are_LinDep )
take v = v; :: thesis: ex 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 & u,v,w are_LinDep )
take w = w; :: thesis: ( p = Dir u & q = Dir v & r = Dir w & not u is zero & not v is zero & not w is zero & u,v,w are_LinDep )
thus ( p = Dir u & q = Dir v & r = Dir w & not u is zero & not v is zero & not w is zero & u,v,w are_LinDep ) by A2; :: thesis: verum

end;

now

assume 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 & u,v,w are_LinDep ) ; :: thesis: p,q,r is_collinear
then [p,q,r] in the Collinearity of (ProjectiveSpace V) by ANPROJ_1:25;
hence p,q,r is_collinear by COLLSP:def 2; :: thesis: verum

end;

hence ( p,q,r is_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 & u,v,w are_LinDep ) ) by A1; :: thesis: verum