for L being LINE of (IncProjSp_of real_projective_plane)
for p, q being POINT of (IncProjSp_of real_projective_plane)
for P, Q being Element of real_projective_plane st p = P & q = Q & P in BK_model & Q in absolute & q on L & p on L holds
ex p1, p2 being POINT of (IncProjSp_of real_projective_plane) ex P1, P2 being Element of real_projective_plane st
( p1 = P1 & p2 = P2 & P1 <> P2 & P1 in absolute & P2 in absolute & p1 on L & p2 on L )