let P, Q be Point of real_projective_plane; :: thesis: ( P <> Q iff dual P <> dual Q )

now :: thesis: ( P <> Q implies not dual P = dual Q )

assume A1: P <> Q ; :: thesis: not dual P = dual Q
assume dual P = dual Q ; :: thesis: contradiction
then P = dual (dual Q) by Th45;
hence contradiction by A1, Th45; :: thesis: verum

end;

hence ( P <> Q iff dual P <> dual Q ) ; :: thesis: verum