for P being Point of (ProjectiveSpace (TOP-REAL 3)) st not P in BK_model \/ absolute holds
ex l being LINE of (IncProjSp_of real_projective_plane) st
( P in l & l misses absolute )