for l1, l2, l3 being Element of ProjectiveLines real_projective_plane st l1,l2,l3 are_concurrent holds
( l2,l1,l3 are_concurrent & l1,l3,l2 are_concurrent & l3,l2,l1 are_concurrent & l3,l2,l1 are_concurrent & l2,l3,l1 are_concurrent ) ;