:: deftheorem defines Pdir2b ANPROJ11:def 14 :
for P being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) holds Pdir2b P = Dir (dir2b P);