for L1, L2 being LINE of real_projective_plane holds L1 meets L2