:: deftheorem Def01 defines L2P BKMODEL1:def 5 :
for p, q being Point of real_projective_plane st p <> q holds
for b₃ being Point of real_projective_plane holds
( b₃ = L2P (p,q) iff ex u, v being non zero Element of (TOP-REAL 3) st
( p = Dir u & q = Dir v & b₃ = Dir (u <X> v) ) );