:: deftheorem defines are_concurrent ANPROJ11:def 26 :
for l1, l2, l3 being Element of ProjectiveLines real_projective_plane holds
( l1,l2,l3 are_concurrent iff ex P being Point of real_projective_plane st
( P in l1 & P in l2 & P in l3 ) );