let P, Q be Element of absolute ; :: thesis: ex R being Element of real_projective_plane st
( R in tangent P & R in tangent Q )
reconsider pP = tangent P, pQ = tangent Q as LINE of (IncProjSp_of real_projective_plane) by INCPROJ:4;
consider R being POINT of (IncProjSp_of real_projective_plane) such that
A1: R on pP and
A2: R on pQ by BKMODEL1:75, INCPROJ:def 9;
reconsider S = R as Element of real_projective_plane by INCPROJ:3;
( S in tangent P & S in tangent Q ) by A1, A2, INCPROJ:5;
hence ex R being Element of real_projective_plane st
( R in tangent P & R in tangent Q ) ; :: thesis: verum