:: deftheorem defines Pdir3a ANPROJ11:def 16 :
for P being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) holds Pdir3a P = Dir (dir3a P);