let L be Element of ProjectiveLines real_projective_plane; :: thesis: ex p, q being Point of real_projective_plane st
( p <> q & L = Line (p,q) )
L in ProjectiveLines real_projective_plane ;
then L in { B where B is Subset of real_projective_plane : B is LINE of real_projective_plane } by INCPROJ:def 1;
then ex B being Subset of real_projective_plane st
( L = B & B is LINE of real_projective_plane ) ;
hence ex p, q being Point of real_projective_plane st
( p <> q & L = Line (p,q) ) by COLLSP:def 7; :: thesis: verum