for P being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3))
for Q being Point of (ProjectiveSpace (TOP-REAL 3)) st Q = Dir (normalize_proj2 P) holds
not Q is zero_proj2 by Def4;