:: deftheorem Def3 defines zero_proj2 ANPROJ11:def 3 :
for P being Point of (ProjectiveSpace (TOP-REAL 3)) holds
( P is zero_proj2 iff for u being non zero Element of (TOP-REAL 3) st P = Dir u holds
u . 2 = 0 );