:: deftheorem defines dual1 ANPROJ11:def 19 :
for P being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) holds dual1 P = Line ((Pdir1a P),(Pdir1b P));