reconsider p = P as Element of real_projective_plane ;
reconsider L = Line (p,(pole_infty P)) as LINE of real_projective_plane by Th19, COLLSP:def 7;
take L ; :: thesis: ex p being Element of real_projective_plane st
( p = P & L = Line (p,(pole_infty P)) )
thus ex p being Element of real_projective_plane st
( p = P & L = Line (p,(pole_infty P)) ) ; :: thesis: verum