let FCPS be up-3-dimensional CollProjectiveSpace; for a, a9, b, b9, c, c9, o, p, q, r being Element of FCPS st not o,a,b are_collinear & not o,b,c are_collinear & not o,a,c are_collinear & o,a,a9 are_collinear & o,b,b9 are_collinear & o,c,c9 are_collinear & a,b,p are_collinear & a9,b9,p are_collinear & a <> a9 & b,c,r are_collinear & b9,c9,r are_collinear & a,c,q are_collinear & b <> b9 & a9,c9,q are_collinear & o <> a9 & o <> b9 & o <> c9 holds
r,q,p are_collinear
let a, a9, b, b9, c, c9, o, p, q, r be Element of FCPS; ( not o,a,b are_collinear & not o,b,c are_collinear & not o,a,c are_collinear & o,a,a9 are_collinear & o,b,b9 are_collinear & o,c,c9 are_collinear & a,b,p are_collinear & a9,b9,p are_collinear & a <> a9 & b,c,r are_collinear & b9,c9,r are_collinear & a,c,q are_collinear & b <> b9 & a9,c9,q are_collinear & o <> a9 & o <> b9 & o <> c9 implies r,q,p are_collinear )
assume that
A1:
not o,a,b are_collinear
and
A2:
not o,b,c are_collinear
and
A3:
not o,a,c are_collinear
and
A4:
( o,a,a9 are_collinear & o,b,b9 are_collinear & o,c,c9 are_collinear )
and
A5:
a,b,p are_collinear
and
A6:
( a9,b9,p are_collinear & a <> a9 )
and
A7:
b,c,r are_collinear
and
A8:
b9,c9,r are_collinear
and
A9:
a,c,q are_collinear
and
A10:
( b <> b9 & a9,c9,q are_collinear & o <> a9 & o <> b9 & o <> c9 )
; r,q,p are_collinear
A11:
now ( a,b,c are_collinear implies r,q,p are_collinear )A12:
(
b <> c &
b,
c,
b are_collinear )
by A2, ANPROJ_2:def 7;
assume A13:
a,
b,
c are_collinear
;
r,q,p are_collinear then
b,
c,
a are_collinear
by Th1;
then A14:
a,
b,
r are_collinear
by A7, A12, ANPROJ_2:def 8;
A15:
(
c <> a &
a,
c,
a are_collinear )
by A3, ANPROJ_2:def 7;
a,
c,
b are_collinear
by A13, Th1;
then A16:
a,
b,
q are_collinear
by A9, A15, ANPROJ_2:def 8;
a <> b
by A1, ANPROJ_2:def 7;
hence
r,
q,
p are_collinear
by A5, A14, A16, ANPROJ_2:def 8;
verum end;
A17:
not o,c,a are_collinear
by A3, Th1;
now ( not a,b,c are_collinear implies r,q,p are_collinear )assume
not
a,
b,
c are_collinear
;
r,q,p are_collinear then
o,
a,
b,
c constitute_a_quadrangle
by A1, A2, A17;
then
p,
r,
q are_collinear
by A4, A5, A6, A7, A8, A9, A10, Lm7;
hence
r,
q,
p are_collinear
by Th1;
verum end;
hence
r,q,p are_collinear
by A11; verum