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

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 ; :: 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;

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

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 ; :: 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 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; :: thesis: verum

end;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; :: thesis: verum

now :: thesis: ( not a,b,c,o are_coplanar implies p,q,r are_collinear )

hence
p,q,r are_collinear
by A20; :: thesis: verumassume A56:
not a,b,c,o are_coplanar
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum