:: deftheorem defines dual3 ANPROJ11:def 21 :
for P being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) holds dual3 P = Line ((Pdir3a P),(Pdir3b P));