for P being Element of (ProjectiveSpace (TOP-REAL 3))
for u being non zero Element of (TOP-REAL 3) st P = Dir u & P in BK_model holds
u . 3 <> 0