let l, m be Element of ProjectiveLines real_projective_plane; :: thesis: ( l <> m iff dual l <> dual m )

now :: thesis: ( l <> m implies not dual l = dual m )

assume A1: l <> m ; :: thesis: not dual l = dual m
assume dual l = dual m ; :: thesis: contradiction
then l = dual (dual m) by Th46;
hence contradiction by A1, Th46; :: thesis: verum

end;

hence ( l <> m iff dual l <> dual m ) ; :: thesis: verum