:: deftheorem Def25 defines dual ANPROJ11:def 25 :
for l being Element of ProjectiveLines real_projective_plane
for b₂ being Point of real_projective_plane holds
( b₂ = dual l iff ex P, Q being Point of real_projective_plane st
( P <> Q & l = Line (P,Q) & b₂ = L2P (P,Q) ) );