for P being Element of real_projective_plane ex Q being Element of BK_model st P <> Q