theorem Th34: :: ANPROJ11:34

for P being non zero_proj2 non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) holds dual2 P = dual3 P