:: deftheorem defines are_Prop_Vect ANPROJ_2:def 1 :
for V being RealLinearSpace
for u, v, w being Element of V holds
( u,v,w are_Prop_Vect iff ( not u is zero & not v is zero & not w is zero ) );