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