let P be Element of real_projective_plane; :: thesis: ( not # P is zero_proj1 implies ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P = P9 & dual P = dual1 P9 ) )
assume A1: not # P is zero_proj1 ; :: thesis: ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P = P9 & dual P = dual1 P9 )
reconsider P1 = # P as non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) by A1;

per cases ( ( not P1 is zero_proj2 & P1 is zero_proj3 ) or ( P1 is zero_proj2 & not P1 is zero_proj3 ) or ( P1 is zero_proj2 & P1 is zero_proj3 ) or ( not P1 is zero_proj2 & not P1 is zero_proj3 ) ) ;

suppose ( not P1 is zero_proj2 & P1 is zero_proj3 ) ; :: thesis: ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P = P9 & dual P = dual1 P9 )

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

end;

suppose ( P1 is zero_proj2 & not P1 is zero_proj3 ) ; :: thesis: ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P = P9 & dual P = dual1 P9 )

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

end;

suppose ( P1 is zero_proj2 & P1 is zero_proj3 ) ; :: thesis: ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P = P9 & dual P = dual1 P9 )

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

end;

suppose ( not P1 is zero_proj2 & not P1 is zero_proj3 ) ; :: thesis: ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P = P9 & dual P = dual1 P9 )

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

end;

end;