theorem Th29: :: BKMODEL3:34

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 )