theorem Th10: :: BKMODEL2:17

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