for P, Q being Element of absolute ex R being Element of real_projective_plane st
( R in tangent P & R in tangent Q )