:: deftheorem Def22 defines dual ANPROJ11:def 22 :
for P being Point of (ProjectiveSpace (TOP-REAL 3))
for b₂ being Element of ProjectiveLines real_projective_plane holds
( ( not P is zero_proj1 implies ( b₂ = dual P iff ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₂ = dual1 P9 ) ) ) & ( P is zero_proj1 & not P is zero_proj2 implies ( b₂ = dual P iff ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₂ = dual2 P9 ) ) ) & ( P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 implies ( b₂ = dual P iff ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₂ = dual3 P9 ) ) ) );