for P being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3))
for Q being Point of (ProjectiveSpace (TOP-REAL 3)) st Q = Dir (normalize_proj1 P) holds
not Q is zero_proj1 by Def2;