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