theorem Th25: :: BKMODEL2:33

for P1, P2 being Element of absolute st P1 <> P2 holds
ex P being Element of real_projective_plane st (tangent P1) /\ (tangent P2) = {P}