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