theorem Th03: :: BKMODEL2:7

for P being Element of BK_model
for Q being Element of (ProjectiveSpace (TOP-REAL 3))
for v being non zero Element of (TOP-REAL 3) st P <> Q & Q = Dir v & v . 3 = 1 holds
ex P1 being Element of absolute st P,Q,P1 are_collinear