let k, l1, l2, l3, m1, m2, m3, n1, n2, n3 be Element of ProjectiveLines real_projective_plane; ( 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 implies n1,n2,n3 are_concurrent )
assume that
A1:
k <> m1
and
A2:
l1 <> m1
and
A3:
k <> m2
and
A4:
l2 <> m2
and
A5:
k <> m3
and
A6:
l3 <> m3
and
A7:
not k,l1,l2 are_concurrent
and
A8:
not k,l1,l3 are_concurrent
and
A9:
not k,l2,l3 are_concurrent
and
A10:
l1,l2,n3 are_concurrent
and
A11:
m1,m2,n3 are_concurrent
and
A12:
l2,l3,n1 are_concurrent
and
A13:
m2,m3,n1 are_concurrent
and
A14:
l1,l3,n2 are_concurrent
and
A15:
m1,m3,n2 are_concurrent
and
A16:
k,l1,m1 are_concurrent
and
A17:
k,l2,m2 are_concurrent
and
A18:
k,l3,m3 are_concurrent
; n1,n2,n3 are_concurrent
( dual k <> dual m1 & dual l1 <> dual m1 & dual k <> dual m2 & dual l2 <> dual m2 & dual k <> dual m3 & dual l3 <> dual m3 & not dual k, dual l1, dual l2 are_collinear & not dual k, dual l1, dual l3 are_collinear & not dual k, dual l2, dual l3 are_collinear & dual l1, dual l2, dual n3 are_collinear & dual m1, dual m2, dual n3 are_collinear & dual l2, dual l3, dual n1 are_collinear & dual m2, dual m3, dual n1 are_collinear & dual l1, dual l3, dual n2 are_collinear & dual m1, dual m3, dual n2 are_collinear & dual k, dual l1, dual m1 are_collinear & dual k, dual l2, dual m2 are_collinear & dual k, dual l3, dual m3 are_collinear )
by A1, A2, A3, A4, A5, A6, Th48, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A18, Th60;
then
dual n1, dual n2, dual n3 are_collinear
by ANPROJ_2:def 12;
hence
n1,n2,n3 are_concurrent
by Th60; verum