for V being RealLinearSpace
for u, v, w, u1, v1, w1 being Element of V st are_Prop u,u1 & are_Prop v,v1 & are_Prop w,w1 & u,v,w are_LinDep holds
u1,v1,w1 are_LinDep