for P being Element of BK_model
for Q being Element of (ProjectiveSpace (TOP-REAL 3)) st P <> Q holds
ex P1 being Element of absolute st P,Q,P1 are_collinear