let FCPS be up-3-dimensional CollProjectiveSpace; for o, a', b', c', a, b, c, p, q, r being Element of st o <> a' & o <> b' & o <> c' & a <> a' & b <> b' & o,a,b,c constitute_a_quadrangle & o,a,a' is_collinear & o,b,b' is_collinear & o,c,c' is_collinear & a,b,p is_collinear & a',b',p is_collinear & b,c,q is_collinear & b',c',q is_collinear & a,c,r is_collinear & a',c',r is_collinear holds
p,q,r is_collinear
let o, a', b', c', a, b, c, p, q, r be Element of ; ( o <> a' & o <> b' & o <> c' & a <> a' & b <> b' & o,a,b,c constitute_a_quadrangle & o,a,a' is_collinear & o,b,b' is_collinear & o,c,c' is_collinear & a,b,p is_collinear & a',b',p is_collinear & b,c,q is_collinear & b',c',q is_collinear & a,c,r is_collinear & a',c',r is_collinear implies p,q,r is_collinear )
assume that
A1:
o <> a'
and
A2:
o <> b'
and
A3:
o <> c'
and
A4:
a <> a'
and
A5:
b <> b'
and
A6:
o,a,b,c constitute_a_quadrangle
and
A7:
o,a,a' is_collinear
and
A8:
o,b,b' is_collinear
and
A9:
o,c,c' is_collinear
and
A10:
a,b,p is_collinear
and
A11:
a',b',p is_collinear
and
A12:
b,c,q is_collinear
and
A13:
b',c',q is_collinear
and
A14:
a,c,r is_collinear
and
A15:
a',c',r is_collinear
; p,q,r is_collinear
A16:
not o,b,c is_collinear
by A6, Def2;
A17:
not a,b,c is_collinear
by A6, Def2;
A18:
not o,c,a is_collinear
by A6, Def2;
A19:
not o,a,b is_collinear
by A6, Def2;
A20:
now assume A21:
a,
b,
c,
o are_coplanar
;
p,q,r is_collinear then A22:
b,
c,
a,
o are_coplanar
by Th11;
A23:
a,
c,
b,
o are_coplanar
by A21, Th11;
consider d being
Element of
such that A24:
not
a,
b,
c,
d are_coplanar
by A17, Th17;
A25:
not
a,
c,
b,
d are_coplanar
by A24, Th11;
A26:
a,
b,
c,
c are_coplanar
by Th18;
A27:
not
b,
c,
a,
d are_coplanar
by A24, Th11;
consider d' being
Element of
such that A28:
o <> d'
and A29:
d <> d'
and A30:
o,
d,
d' is_collinear
by ANPROJ_2:def 10;
a,
o,
a' is_collinear
by A7, Th1;
then consider s being
Element of
such that A31:
a,
d,
s is_collinear
and A32:
a',
d',
s is_collinear
by A30, ANPROJ_2:def 9;
A33:
d,
a,
s is_collinear
by A31, Th1;
b,
o,
b' is_collinear
by A8, Th1;
then consider t being
Element of
such that A34:
(
b,
d,
t is_collinear &
b',
d',
t is_collinear )
by A30, ANPROJ_2:def 9;
c,
o,
c' is_collinear
by A9, Th1;
then consider u being
Element of
such that A35:
c,
d,
u is_collinear
and A36:
c',
d',
u is_collinear
by A30, ANPROJ_2:def 9;
A37:
s,
t,
u,
s are_coplanar
by Th18;
not
a,
c,
o is_collinear
by A18, Th1;
then A38:
not
a,
c,
d,
o are_coplanar
by A25, A23, Th22;
then
not
a',
c',
d' is_collinear
by A1, A3, A7, A9, A28, A30, Th23;
then
r,
u,
s is_collinear
by A4, A7, A14, A15, A31, A32, A35, A36, A38, Th21;
then A39:
s,
u,
r is_collinear
by Th1;
not
a,
b,
o is_collinear
by A19, Th1;
then A40:
not
a,
b,
d,
o are_coplanar
by A21, A24, Th22;
then
not
d,
o,
a is_collinear
by Th10;
then A41:
not
o,
d,
a is_collinear
by Th1;
A42:
s,
t,
u,
u are_coplanar
by Th18;
not
b,
c,
o is_collinear
by A16, Th1;
then A43:
not
b,
c,
d,
o are_coplanar
by A27, A22, Th22;
then
not
b',
c',
d' is_collinear
by A2, A3, A8, A9, A28, A30, Th23;
then
q,
u,
t is_collinear
by A5, A8, A12, A13, A34, A35, A36, A43, Th21;
then A44:
u,
t,
q is_collinear
by Th1;
A45:
s,
t,
u,
t are_coplanar
by Th18;
d',
a',
s is_collinear
by A32, Th1;
then
s <> a
by A4, A7, A28, A30, A41, Th8;
then A46:
not
a,
b,
c,
s are_coplanar
by A24, A33, Th19;
A47:
a,
b,
c,
b are_coplanar
by Th18;
not
a',
b',
d' is_collinear
by A1, A2, A7, A8, A28, A30, A40, Th23;
then
p,
t,
s is_collinear
by A4, A7, A10, A11, A31, A32, A34, A40, Th21;
then A48:
t,
s,
p is_collinear
by Th1;
A49:
a,
b,
c,
a are_coplanar
by Th18;
A50:
not
s,
t,
u is_collinear
by A1, A2, A7, A8, A21, A24, A29, A30, A31, A32, A34, A35, A40, Th24;
then
t <> u
by ANPROJ_2:def 7;
then A51:
s,
t,
u,
q are_coplanar
by A44, A45, A42, Th14;
c <> a
by A18, ANPROJ_2:def 7;
then A52:
a,
b,
c,
r are_coplanar
by A14, A49, A26, Th14;
b <> c
by A16, ANPROJ_2:def 7;
then A53:
a,
b,
c,
q are_coplanar
by A12, A47, A26, Th14;
a <> b
by A19, ANPROJ_2:def 7;
then A54:
a,
b,
c,
p are_coplanar
by A10, A49, A47, Th14;
u <> s
by A50, ANPROJ_2:def 7;
then A55:
s,
t,
u,
r are_coplanar
by A39, A37, A42, Th14;
s <> t
by A50, ANPROJ_2:def 7;
then
s,
t,
u,
p are_coplanar
by A48, A37, A45, Th14;
hence
p,
q,
r is_collinear
by A17, A50, A46, A54, A53, A52, A51, A55, Th20;
verum end;
now assume A56:
not
a,
b,
c,
o are_coplanar
;
p,q,r is_collinear then
not
a',
b',
c' is_collinear
by A1, A2, A3, A7, A8, A9, Th23;
hence
p,
q,
r is_collinear
by A4, A7, A10, A11, A12, A13, A14, A15, A56, Th21;
verum end;
hence
p,q,r is_collinear
by A20; verum