for l, m, n being Element of ProjectiveLines real_projective_plane holds
( l,m,l are_concurrent & l,l,m are_concurrent & l,m,m are_concurrent )