:: deftheorem Def6 defines normalize_proj3 ANPROJ11:def 6 :
for P being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3))
for b₂ being non zero Element of (TOP-REAL 3) holds
( b₂ = normalize_proj3 P iff ( Dir b₂ = P & b₂ . 3 = 1 ) );