theorem :: BKMODEL1:72

for L being Element of ProjectiveLines real_projective_plane ex p, q being Point of real_projective_plane st
( p <> q & L = Line (p,q) )