let P be Point of real_projective_plane; :: thesis: for l being Element of ProjectiveLines real_projective_plane st dual l in dual P holds
P in l
let l be Element of ProjectiveLines real_projective_plane; :: thesis: ( dual l in dual P implies P in l )
assume dual l in dual P ; :: thesis: P in l
then dual (dual P) in dual (dual l) by Th54;
then P in dual (dual l) by Th45;
hence P in l by Th46; :: thesis: verum