let k, l1, l2, l3, m1, m2, m3, n1, n2, n3 be Element of ProjectiveLines real_projective_plane; :: thesis: ( k <> l2 & k <> l3 & l2 <> l3 & l1 <> l2 & l1 <> l3 & k <> m2 & k <> m3 & m2 <> m3 & m1 <> m2 & m1 <> m3 & not k,l1,m1 are_concurrent & k,l1,l2 are_concurrent & k,l1,l3 are_concurrent & k,m1,m2 are_concurrent & k,m1,m3 are_concurrent & l1,m2,n3 are_concurrent & m1,l2,n3 are_concurrent & l1,m3,n2 are_concurrent & l3,m1,n2 are_concurrent & l2,m3,n1 are_concurrent & l3,m2,n1 are_concurrent implies n1,n2,n3 are_concurrent )
assume that
A1: k <> l2 and
A2: k <> l3 and
A3: l2 <> l3 and
A4: l1 <> l2 and
A5: l1 <> l3 and
A6: k <> m2 and
A7: k <> m3 and
A8: m2 <> m3 and
A9: m1 <> m2 and
A10: m1 <> m3 and
A11: not k,l1,m1 are_concurrent and
A12: k,l1,l2 are_concurrent and
A13: k,l1,l3 are_concurrent and
A14: k,m1,m2 are_concurrent and
A15: k,m1,m3 are_concurrent and
A16: l1,m2,n3 are_concurrent and
A17: m1,l2,n3 are_concurrent and
A18: l1,m3,n2 are_concurrent and
A19: l3,m1,n2 are_concurrent and
A20: l2,m3,n1 are_concurrent and
A21: l3,m2,n1 are_concurrent ; :: thesis: n1,n2,n3 are_concurrent

now :: thesis: ( dual k <> dual l2 & dual k <> dual l3 & dual l2 <> dual l3 & dual l1 <> dual l2 & dual l1 <> dual l3 & dual k <> dual m2 & dual k <> dual m3 & dual m2 <> dual m3 & dual m1 <> dual m2 & dual m1 <> dual m3 & not dual k, dual l1, dual m1 are_collinear & dual k, dual l1, dual l2 are_collinear & dual k, dual l1, dual l3 are_collinear & dual k, dual m1, dual m2 are_collinear & dual k, dual m1, dual m3 are_collinear & dual l1, dual m2, dual n3 are_collinear & dual m1, dual l2, dual n3 are_collinear & dual l1, dual m3, dual n2 are_collinear & dual l3, dual m1, dual n2 are_collinear & dual l2, dual m3, dual n1 are_collinear & dual l3, dual m2, dual n1 are_collinear )

thus ( dual k <> dual l2 & dual k <> dual l3 & dual l2 <> dual l3 ) by A1, A2, A3, Th48; :: thesis: ( dual l1 <> dual l2 & dual l1 <> dual l3 & dual k <> dual m2 & dual k <> dual m3 & dual m2 <> dual m3 & dual m1 <> dual m2 & dual m1 <> dual m3 & not dual k, dual l1, dual m1 are_collinear & dual k, dual l1, dual l2 are_collinear & dual k, dual l1, dual l3 are_collinear & dual k, dual m1, dual m2 are_collinear & dual k, dual m1, dual m3 are_collinear & dual l1, dual m2, dual n3 are_collinear & dual m1, dual l2, dual n3 are_collinear & dual l1, dual m3, dual n2 are_collinear & dual l3, dual m1, dual n2 are_collinear & dual l2, dual m3, dual n1 are_collinear & dual l3, dual m2, dual n1 are_collinear )
thus ( dual l1 <> dual l2 & dual l1 <> dual l3 & dual k <> dual m2 ) by A4, A5, A6, Th48; :: thesis: ( dual k <> dual m3 & dual m2 <> dual m3 & dual m1 <> dual m2 & dual m1 <> dual m3 & not dual k, dual l1, dual m1 are_collinear & dual k, dual l1, dual l2 are_collinear & dual k, dual l1, dual l3 are_collinear & dual k, dual m1, dual m2 are_collinear & dual k, dual m1, dual m3 are_collinear & dual l1, dual m2, dual n3 are_collinear & dual m1, dual l2, dual n3 are_collinear & dual l1, dual m3, dual n2 are_collinear & dual l3, dual m1, dual n2 are_collinear & dual l2, dual m3, dual n1 are_collinear & dual l3, dual m2, dual n1 are_collinear )
thus ( dual k <> dual m3 & dual m2 <> dual m3 & dual m1 <> dual m2 & dual m1 <> dual m3 ) by A7, A8, A9, A10, Th48; :: thesis: ( not dual k, dual l1, dual m1 are_collinear & dual k, dual l1, dual l2 are_collinear & dual k, dual l1, dual l3 are_collinear & dual k, dual m1, dual m2 are_collinear & dual k, dual m1, dual m3 are_collinear & dual l1, dual m2, dual n3 are_collinear & dual m1, dual l2, dual n3 are_collinear & dual l1, dual m3, dual n2 are_collinear & dual l3, dual m1, dual n2 are_collinear & dual l2, dual m3, dual n1 are_collinear & dual l3, dual m2, dual n1 are_collinear )
thus ( not dual k, dual l1, dual m1 are_collinear & dual k, dual l1, dual l2 are_collinear & dual k, dual l1, dual l3 are_collinear & dual k, dual m1, dual m2 are_collinear & dual k, dual m1, dual m3 are_collinear & dual l1, dual m2, dual n3 are_collinear & dual m1, dual l2, dual n3 are_collinear & dual l1, dual m3, dual n2 are_collinear & dual l3, dual m1, dual n2 are_collinear & dual l2, dual m3, dual n1 are_collinear & dual l3, dual m2, dual n1 are_collinear ) by A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, A21, Th60; :: thesis: verum

end;

then dual n1, dual n2, dual n3 are_collinear by ANPROJ_2:def 13;
hence n1,n2,n3 are_concurrent by Th60; :: thesis: verum