let L be LINE of (IncProjSp_of real_projective_plane); :: thesis: ex p, q being Point of real_projective_plane st
( p <> q & L = Line (p,q) )
L in the Lines of (IncProjSp_of real_projective_plane) ;
then L in ProjectiveLines real_projective_plane by INCPROJ:2;
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