let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for o, a', b', c', a, b, c, p, q, r being Element of FCPS 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 FCPS; :: thesis: ( 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' & o <> b' & o <> c' & a <> a' & b <> b' )
and
A2:
o,a,b,c constitute_a_quadrangle
and
A3:
( 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 )
; :: thesis: p,q,r is_collinear
A4:
( o <> a' & o <> b' & o <> c' & a <> a' & b <> b' & not o,a,b is_collinear & not o,b,c is_collinear & not o,c,a is_collinear & not a,b,c is_collinear & 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 )
by A1, A2, A3, Def2;
A5:
now assume A6:
not
a,
b,
c,
o are_coplanar
;
:: thesis: p,q,r is_collinear then
not
a',
b',
c' is_collinear
by A1, A3, Th23;
hence
p,
q,
r is_collinear
by A1, A3, A6, Th21;
:: thesis: verum end;
now assume A7:
a,
b,
c,
o are_coplanar
;
:: thesis: p,q,r is_collinear consider d being
Element of
FCPS such that A8:
not
a,
b,
c,
d are_coplanar
by A4, Th17;
consider d' being
Element of
FCPS such that A9:
(
o <> d' &
d <> d' &
o,
d,
d' is_collinear )
by ANPROJ_2:def 10;
A10:
(
a,
o,
a' is_collinear &
b,
o,
b' is_collinear &
c,
o,
c' is_collinear )
by A3, Th1;
then consider s being
Element of
FCPS such that A11:
(
a,
d,
s is_collinear &
a',
d',
s is_collinear )
by A9, ANPROJ_2:def 9;
consider t being
Element of
FCPS such that A12:
(
b,
d,
t is_collinear &
b',
d',
t is_collinear )
by A9, A10, ANPROJ_2:def 9;
consider u being
Element of
FCPS such that A13:
(
c,
d,
u is_collinear &
c',
d',
u is_collinear )
by A9, A10, ANPROJ_2:def 9;
A14:
( not
a,
b,
o is_collinear & not
b,
c,
o is_collinear & not
a,
c,
o is_collinear )
by A4, Th1;
then A15:
not
a,
b,
d,
o are_coplanar
by A7, A8, Th22;
( not
b,
c,
a,
d are_coplanar &
b,
c,
a,
o are_coplanar )
by A7, A8, Th11;
then A16:
not
b,
c,
d,
o are_coplanar
by A14, Th22;
( not
a,
c,
b,
d are_coplanar &
a,
c,
b,
o are_coplanar )
by A7, A8, Th11;
then A17:
not
a,
c,
d,
o are_coplanar
by A14, Th22;
then A18:
not
s,
t,
u is_collinear
by A1, A3, A7, A8, A9, A11, A12, A13, A15, A16, Th24;
not
a',
b',
d' is_collinear
by A1, A3, A9, A15, Th23;
then
p,
t,
s is_collinear
by A1, A3, A11, A12, A15, Th21;
then A19:
t,
s,
p is_collinear
by Th1;
not
b',
c',
d' is_collinear
by A1, A3, A9, A16, Th23;
then
q,
u,
t is_collinear
by A1, A3, A12, A13, A16, Th21;
then A20:
u,
t,
q is_collinear
by Th1;
not
a',
c',
d' is_collinear
by A1, A3, A9, A17, Th23;
then
r,
u,
s is_collinear
by A1, A3, A11, A13, A17, Th21;
then A21:
s,
u,
r is_collinear
by Th1;
A22:
(
d,
a,
s is_collinear &
d',
a',
s is_collinear )
by A11, Th1;
not
d,
o,
a is_collinear
by A15, Th10;
then
not
o,
d,
a is_collinear
by Th1;
then
s <> a
by A1, A3, A9, A22, Th8;
then A23:
not
a,
b,
c,
s are_coplanar
by A8, A22, Th19;
A24:
(
a <> b &
b <> c &
c <> a &
s <> t &
t <> u &
u <> s )
by A4, A18, ANPROJ_2:def 7;
A25:
(
a,
b,
c,
a are_coplanar &
a,
b,
c,
b are_coplanar &
a,
b,
c,
c are_coplanar &
s,
t,
u,
s are_coplanar &
s,
t,
u,
t are_coplanar &
s,
t,
u,
u are_coplanar )
by Th18;
then A26:
(
a,
b,
c,
p are_coplanar &
a,
b,
c,
q are_coplanar &
a,
b,
c,
r are_coplanar )
by A3, A24, Th14;
(
s,
t,
u,
p are_coplanar &
s,
t,
u,
q are_coplanar &
s,
t,
u,
r are_coplanar )
by A19, A20, A21, A24, A25, Th14;
hence
p,
q,
r is_collinear
by A4, A18, A23, A26, Th20;
:: thesis: verum end;
hence
p,q,r is_collinear
by A5; :: thesis: verum