theorem :: BKMODEL2:8

for P being Element of BK_model
for L being LINE of (IncProjSp_of real_projective_plane) ex Q being Element of (ProjectiveSpace (TOP-REAL 3)) st
( P <> Q & Q in L )