for P, Q being Element of BK_model
for P1, P2, P3 being Element of absolute st P <> Q & P1 <> P2 & P,Q,P1 are_collinear & P,Q,P2 are_collinear & P,Q,P3 are_collinear & not P3 = P1 holds
P3 = P2