for V being non trivial RealLinearSpace
for p, q being Element of V st not p is zero & not q is zero holds
( Dir p = Dir q iff are_Prop p,q )