:: deftheorem defines Dir ANPROJ_1:def 4 :
for V being RealLinearSpace
for v being Element of V holds Dir v = Class ((Proportionality_as_EqRel_of V),v);