theorem Th59: :: ANPROJ11:59
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 )