:: deftheorem defines dir2a ANPROJ11:def 11 :
for P being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) holds dir2a P = |[1,(- ((normalize_proj2 P) . 1)),0]|;