let P be Point of real_projective_plane; :: thesis: not P in dual P
reconsider P9 = P as Element of (ProjectiveSpace (TOP-REAL 3)) ;
per cases ( not P9 is zero_proj1 or not P9 is zero_proj2 or not P9 is zero_proj3 ) by Th37;
suppose not P9 is zero_proj1 ; :: thesis: not P in dual P
then reconsider P9 = P as non zero_proj1 Element of (ProjectiveSpace (TOP-REAL 3)) ;
# P = P9 ;
then consider P99 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) such that
A1: P = P99 and
A2: dual P = dual1 P99 by Th38;
assume P in dual P ; :: thesis: contradiction
hence contradiction by A1, A2, Th41; :: thesis: verum
end;
suppose not P9 is zero_proj2 ; :: thesis: not P in dual P
then reconsider P9 = P as non zero_proj2 Element of (ProjectiveSpace (TOP-REAL 3)) ;
# P = P9 ;
then consider P99 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) such that
A3: P = P99 and
A4: dual P = dual2 P99 by Th39;
assume P in dual P ; :: thesis: contradiction
hence contradiction by Th42, A3, A4; :: thesis: verum
end;
suppose not P9 is zero_proj3 ; :: thesis: not P in dual P
then reconsider P9 = P as non zero_proj3 Element of (ProjectiveSpace (TOP-REAL 3)) ;
# P = P9 ;
then consider P99 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) such that
A5: P = P99 and
A6: dual P = dual3 P99 by Th40;
assume P in dual P ; :: thesis: contradiction
hence contradiction by Th43, A5, A6; :: thesis: verum
end;
end;