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