:: deftheorem Def03 defines pole_infty BKMODEL2:def 4 :
for P being Element of absolute
for b₂ being Element of real_projective_plane holds
( b₂ = pole_infty P iff ex u being non zero Element of (TOP-REAL 3) st
( P = Dir u & u . 3 = 1 & ((u . 1) ^2) + ((u . 2) ^2) = 1 & b₂ = Dir |[(- (u . 2)),(u . 1),0]| ) );