let k, l1, l2, l3, m1, m2, m3, n1, n2, n3 be Element of ProjectiveLines real_projective_plane; ( 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
; n1,n2,n3 are_concurrent
now ( 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;
( 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;
( 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;
( 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;
verum end;
then
dual n1, dual n2, dual n3 are_collinear
by ANPROJ_2:def 13;
hence
n1,n2,n3 are_concurrent
by Th60; verum