for l1, l2, l3 being Element of ProjectiveLines real_projective_plane holds
( l1,l2,l3 are_concurrent iff # l1, # l2, # l3 are_concurrent )