let P1, P2 be Element of absolute ; :: thesis: ( P1 <> P2 implies ex P being Element of real_projective_plane st (tangent P1) /\ (tangent P2) = {P} )
assume P1 <> P2 ; :: thesis: ex P being Element of real_projective_plane st (tangent P1) /\ (tangent P2) = {P}
then tangent P1 <> tangent P2 by Th23;
hence ex P being Element of real_projective_plane st (tangent P1) /\ (tangent P2) = {P} by COLLSP:21, BKMODEL1:76; :: thesis: verum