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