for P, Q being Element of real_projective_plane st P in absolute & Q in BK_model holds
ex R being Element of real_projective_plane st
( R in BK_model & Q <> R & R,Q,P are_collinear )