for P, Q, R being Point of real_projective_plane holds
( P,Q,R are_collinear iff dual P, dual Q, dual R are_concurrent )