let P be Element of real_projective_plane; :: thesis:
assume A1: not # P is zero_proj3 ; :: thesis:
reconsider P1 = # P as non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) by A1;

suppose A2: ( not P1 is zero_proj2 & P1 is zero_proj1 ) ; :: thesis:

then reconsider P9 = P as non zero_proj2 non zero_proj3 Element of (ProjectiveSpace (TOP-REAL 3)) ;
( dual P1 = dual2 P9 & dual3 P9 = dual2 P9 ) by A2, Def22, Th34;
hence ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P = P9 & dual P = dual3 P9 ) ; :: thesis:

end;

suppose ( P1 is zero_proj2 & not P1 is zero_proj1 ) ; :: thesis:

then reconsider P9 = P as non zero_proj1 non zero_proj3 Element of (ProjectiveSpace (TOP-REAL 3)) ;
( dual P1 = dual1 P9 & dual1 P9 = dual3 P9 ) by Def22, Th35;
hence ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P = P9 & dual P = dual3 P9 ) ; :: thesis:

end;

suppose ( P1 is zero_proj2 & P1 is zero_proj1 ) ; :: thesis:

hence ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P = P9 & dual P = dual3 P9 ) by Def22; :: thesis:

end;

suppose ( not P1 is zero_proj2 & not P1 is zero_proj1 ) ; :: thesis:

then reconsider P9 = P as non zero_proj1 non zero_proj2 non zero_proj3 Element of (ProjectiveSpace (TOP-REAL 3)) ;
( dual P1 = dual1 P9 & dual1 P9 = dual3 P9 ) by Th35, Def22;
hence ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P = P9 & dual P = dual3 P9 ) ; :: thesis:

end;

end;