:: deftheorem defines Pdir1a ANPROJ11:def 8 :
for P being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) holds Pdir1a P = Dir (dir1a P);