for p, q being Point of real_projective_plane st p <> q holds
( L2P (q,p) = L2P (p,q) & p <> L2P (p,q) )