for x being object
for V being non trivial RealLinearSpace holds
( x is Element of (ProjectiveSpace V) iff ex u being Element of V st
( not u is zero & x = Dir u ) )