theorem Th09: :: BKMODEL2:16

for L being LINE of (IncProjSp_of real_projective_plane)
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 L & u . 3 <> 0 holds
ex Q being Element of (ProjectiveSpace (TOP-REAL 3)) ex v being non zero Element of (TOP-REAL 3) st
( Q = Dir v & Q in L & P <> Q & v . 3 <> 0 )