let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: 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; :: thesis: ( 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
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 ; :: thesis: 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 :: thesis: ( a,b,c,o are_coplanar implies p,q,r are_collinear )
assume A21: a,b,c,o are_coplanar ; :: thesis: p,q,r are_collinear
then A22: b,c,a,o are_coplanar by Th7;
A23: a,c,b,o are_coplanar by ;
consider d being Element of FCPS such that
A24: not a,b,c,d are_coplanar by ;
A25: not a,c,b,d are_coplanar by ;
A26: a,b,c,c are_coplanar by Th14;
A27: not b,c,a,d are_coplanar by ;
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 ;
then consider s being Element of FCPS such that
A31: a,d,s are_collinear and
A32: a9,d9,s are_collinear by ;
A33: d,a,s are_collinear by ;
b,o,b9 are_collinear by ;
then consider t being Element of FCPS such that
A34: ( b,d,t are_collinear & b9,d9,t are_collinear ) by ;
c,o,c9 are_collinear by ;
then consider u being Element of FCPS such that
A35: c,d,u are_collinear and
A36: c9,d9,u are_collinear by ;
A37: s,t,u,s are_coplanar by Th14;
not a,c,o are_collinear by ;
then A38: not a,c,d,o are_coplanar by ;
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 ;
then A40: not a,b,d,o are_coplanar by ;
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 ;
then A43: not b,c,d,o are_coplanar by ;
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 ;
then s <> a by A4, A7, A28, A30, A41, Th5;
then A46: not a,b,c,s are_coplanar by ;
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 ;
c <> a by ;
then A52: a,b,c,r are_coplanar by ;
b <> c by ;
then A53: a,b,c,q are_coplanar by ;
a <> b by ;
then A54: a,b,c,p are_coplanar by ;
u <> s by ;
then A55: s,t,u,r are_coplanar by ;
s <> t by ;
then s,t,u,p are_coplanar by ;
hence p,q,r are_collinear by A17, A50, A46, A54, A53, A52, A51, A55, Th16; :: thesis: verum
end;
now :: thesis: ( not a,b,c,o are_coplanar implies p,q,r are_collinear )end;
hence p,q,r are_collinear by A20; :: thesis: verum