:: deftheorem defines dir3a ANPROJ11:def 15 :
for P being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) holds dir3a P = |[1,0,(- ((normalize_proj3 P) . 1))]|;