let l1, n2, m, n1, m1, l, n be Element of ProjectiveLines real_projective_plane; :: thesis: ( l1,n2,m are_concurrent & n1,m1,m are_concurrent & l1,n1,l are_concurrent & n2,m1,l are_concurrent & l1,m1,n are_concurrent & n2,n1,n are_concurrent & l,m,n are_concurrent & not l1,n2,m1 are_concurrent & not l1,n2,n1 are_concurrent & not l1,n1,m1 are_concurrent implies n2,n1,m1 are_concurrent )
assume that
A1: l1,n2,m are_concurrent and
A2: n1,m1,m are_concurrent and
A3: l1,n1,l are_concurrent and
A4: n2,m1,l are_concurrent and
A5: l1,m1,n are_concurrent and
A6: n2,n1,n are_concurrent and
A7: l,m,n are_concurrent ; :: thesis: ( l1,n2,m1 are_concurrent or l1,n2,n1 are_concurrent or l1,n1,m1 are_concurrent or n2,n1,m1 are_concurrent )
( dual l1, dual n2, dual m are_collinear & dual n1, dual m1, dual m are_collinear & dual l1, dual n1, dual l are_collinear & dual n2, dual m1, dual l are_collinear & dual l1, dual m1, dual n are_collinear & dual n2, dual n1, dual n are_collinear & dual l, dual m, dual n are_collinear ) by A1, A2, A3, A4, A5, A6, A7, Th60;
then ( dual l1, dual n2, dual m1 are_collinear or dual l1, dual n2, dual n1 are_collinear or dual l1, dual n1, dual m1 are_collinear or dual n2, dual n1, dual m1 are_collinear ) by ANPROJ_2:def 11;
hence ( l1,n2,m1 are_concurrent or l1,n2,n1 are_concurrent or l1,n1,m1 are_concurrent or n2,n1,m1 are_concurrent ) by Th60; :: thesis: verum