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