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) )