theorem Th60: :: BKMODEL1:73

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