for P being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3))
for Q being Point of (ProjectiveSpace (TOP-REAL 3)) st Q = Dir (normalize_proj3 P) holds
not Q is zero_proj3 by Def6;