for l being Element of ProjectiveLines real_projective_plane
for P, Q, R being Point of real_projective_plane st P in l & Q in l & R in l holds
P,Q,R are_collinear