for P, PP1, PP2 being Element of real_projective_plane
for P1, P2 being Element of absolute
for Q being Element of real_projective_plane st P1 <> P2 & PP1 = P1 & PP2 = P2 & P in BK_model & P,PP1,PP2 are_collinear & Q in tangent P1 & Q in tangent P2 holds
ex R being Element of real_projective_plane st
( R in absolute & P,Q,R are_collinear )