theorem Th38: :: ANPROJ11:38

for P being Element of real_projective_plane st not # P is zero_proj1 holds
ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P = P9 & dual P = dual1 P9 )