for P, Q, R being Element of real_projective_plane st P,Q,R are_collinear holds
( Q,R,P are_collinear & R,P,Q are_collinear & P,R,Q are_collinear & R,Q,P are_collinear & Q,P,R are_collinear ) by ANPROJ_2:24;