let V be non trivial RealLinearSpace; :: thesis: for u, v, w being Element of V st not u is zero & not v is zero & not w is zero holds
( [(Dir u),(Dir v),(Dir w)] in the Collinearity of (ProjectiveSpace V) iff u,v,w are_LinDep )
let u, v, w be Element of V; :: thesis: ( not u is zero & not v is zero & not w is zero implies ( [(Dir u),(Dir v),(Dir w)] in the Collinearity of (ProjectiveSpace V) iff u,v,w are_LinDep ) )
assume that
A1: ( not u is zero & not v is zero ) and
A2: not w is zero ; :: thesis: ( [(Dir u),(Dir v),(Dir w)] in the Collinearity of (ProjectiveSpace V) iff u,v,w are_LinDep )

now :: thesis: ( [(Dir u),(Dir v),(Dir w)] in the Collinearity of (ProjectiveSpace V) implies u,v,w are_LinDep )

reconsider du = Dir u, dv = Dir v, dw = Dir w as set ;
assume [(Dir u),(Dir v),(Dir w)] in the Collinearity of (ProjectiveSpace V) ; :: thesis: u,v,w are_LinDep
then consider p, q, r being Element of V such that
A3: ( du = Dir p & dv = Dir q ) and
A4: dw = Dir r and
A5: ( not p is zero & not q is zero ) and
A6: not r is zero and
A7: p,q,r are_LinDep by Def6;
A8: are_Prop r,w by A2, A4, A6, Th22;
( are_Prop p,u & are_Prop q,v ) by A1, A3, A5, Th22;
hence u,v,w are_LinDep by A7, A8, Th4; :: thesis: verum

end;

hence ( [(Dir u),(Dir v),(Dir w)] in the Collinearity of (ProjectiveSpace V) iff u,v,w are_LinDep ) by A1, A2, Def6; :: thesis: verum