for V being non trivial RealLinearSpace
for p being Element of V st not p is zero holds
Dir p is Element of ProjectivePoints V