let V be non trivial RealLinearSpace; :: thesis: 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 ) ) ) )
let p, q, r be Element of (ProjectiveSpace V); :: thesis: ( 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 ) ) ) )

hereby :: 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 & ex a, b, c being Real st
( ((a * u) + (b * v)) + (c * w) = 0. V & ( a <> 0 or b <> 0 or c <> 0 ) ) ) implies p,q,r are_collinear )

assume p,q,r are_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 & ex a, b, c being Real st
( ((a * u) + (b * v)) + (c * w) = 0. V & ( a <> 0 or b <> 0 or c <> 0 ) ) )
then consider u, v, w being Element of V such that
A1: ( 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_2:23;
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 & ex a, b, c being Real st
( ((a * u) + (b * v)) + (c * w) = 0. V & ( a <> 0 or b <> 0 or c <> 0 ) ) )
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 & ex a, b, c being Real st
( ((a * u) + (b * v)) + (c * w) = 0. V & ( a <> 0 or b <> 0 or c <> 0 ) ) )
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 & ex a, b, c being Real st
( ((a * u) + (b * v)) + (c * w) = 0. V & ( a <> 0 or b <> 0 or c <> 0 ) ) )
thus ( 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 ) ) ) by A1, ANPROJ_1:def 2; :: thesis: verum

end;

given 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 & ex a, b, c being Real st
( ((a * u) + (b * v)) + (c * w) = 0. V & ( a <> 0 or b <> 0 or c <> 0 ) ) ) ; :: thesis: p,q,r are_collinear
( 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, ANPROJ_1:def 2;
hence p,q,r are_collinear by ANPROJ_2:23; :: thesis: verum