for l1, l2, l3 being LINE of (IncProjSp_of real_projective_plane) holds
( l1,l2,l3 are_concurrent iff # l1, # l2, # l3 are_concurrent )