for l, l1, m, m1 being Element of ProjectiveLines real_projective_plane ex n being Element of ProjectiveLines real_projective_plane st
( l,l1,n are_concurrent & m,m1,n are_concurrent )