for V being RealLinearSpace
for u, v, w being Element of V st not u,v,w are_LinDep holds
( not u is zero & not v is zero & not w is zero & not are_Prop u,v & not are_Prop v,w & not are_Prop w,u ) by Th10, Th11;