:: deftheorem defines dir1a ANPROJ11:def 7 :
for P being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) holds dir1a P = |[(- ((normalize_proj1 P) . 2)),1,0]|;