reconsider P1 = Pdir1a P, P2 = Pdir1b P as Point of real_projective_plane ;
reconsider L = Line (P1,P2) as LINE of real_projective_plane by Th20, COLLSP:def 7;
L in { B where B is Subset of real_projective_plane : B is LINE of real_projective_plane } ;
hence Line ((Pdir1a P),(Pdir1b P)) is Element of ProjectiveLines real_projective_plane ; :: thesis: verum