theorem :: BKMODEL1:86

for P being Point of (ProjectiveSpace (TOP-REAL 3))
for u being non zero Element of (TOP-REAL 3) st P = Dir u & u . 3 = 1 holds
( |[(u . 1),(u . 2)]| in circle (0,0,1) iff P is Element of absolute ) by Th68, Th69;