:: deftheorem defines dual2 ANPROJ11:def 20 :
for P being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) holds dual2 P = Line ((Pdir2a P),(Pdir2b P));