theorem Th40: :: ANPROJ11:40

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