:: deftheorem Def01 defines # BKMODEL3:def 1 :
for P being Element of real_projective_plane st P in absolute \/ BK_model holds
for b₂ being non zero Element of (TOP-REAL 3) holds
( b₂ = # P iff ( Dir b₂ = P & b₂ . 3 = 1 ) );