theorem Th54: :: ANPROJ11:54

for P being Point of real_projective_plane
for l being Element of ProjectiveLines real_projective_plane st P in l holds
dual l in dual P