:: deftheorem Def05 defines RP3_to_REAL2 BKMODEL4:def 5 :
for P being non point_at_infty Point of (ProjectiveSpace (TOP-REAL 3))
for b₂ being Element of REAL 2 holds
( b₂ = RP3_to_REAL2 P iff ex u being non zero Element of (TOP-REAL 3) st
( P = Dir u & u `3 = 1 & b<sub>2</sub> = |[(u `1),(u `2)]| ) );