:: deftheorem Def04 defines tangent BKMODEL2:def 5 :
for P being Element of absolute
for b₂ being LINE of real_projective_plane holds
( b₂ = tangent P iff ex p being Element of real_projective_plane st
( p = P & b₂ = Line (p,(pole_infty P)) ) );