for k, l1, l2, l3, m1, m2, m3, n1, n2, n3 being Element of ProjectiveLines real_projective_plane st k <> m1 & l1 <> m1 & k <> m2 & l2 <> m2 & k <> m3 & l3 <> m3 & not k,l1,l2 are_concurrent & not k,l1,l3 are_concurrent & not k,l2,l3 are_concurrent & l1,l2,n3 are_concurrent & m1,m2,n3 are_concurrent & l2,l3,n1 are_concurrent & m2,m3,n1 are_concurrent & l1,l3,n2 are_concurrent & m1,m3,n2 are_concurrent & k,l1,m1 are_concurrent & k,l2,m2 are_concurrent & k,l3,m3 are_concurrent holds
n1,n2,n3 are_concurrent