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

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

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

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

end;

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

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

end;

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

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

end;

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

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 = dual2 P9 ) by Def22, Th33;
hence ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P = P9 & dual P = dual2 P9 ) ; :: thesis: verum

end;

end;