:: deftheorem Def4 defines normalize_proj2 ANPROJ11:def 4 :
for P being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3))
for b₂ being non zero Element of (TOP-REAL 3) holds
( b₂ = normalize_proj2 P iff ( Dir b₂ = P & b₂ . 2 = 1 ) );