let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for a, b, c, p, q, r, s being Element of FCPS st not p,q,r are_collinear & a,b,c,p are_coplanar & a,b,c,r are_coplanar & a,b,c,q are_coplanar & p,q,r,s are_coplanar holds
a,b,c,s are_coplanar
let a, b, c, p, q, r, s be Element of FCPS; :: thesis: ( not p,q,r are_collinear & a,b,c,p are_coplanar & a,b,c,r are_coplanar & a,b,c,q are_coplanar & p,q,r,s are_coplanar implies a,b,c,s are_coplanar )
assume that
A1: not p,q,r are_collinear and
A2: a,b,c,p are_coplanar and
A3: a,b,c,r are_coplanar and
A4: a,b,c,q are_coplanar and
A5: p,q,r,s are_coplanar ; :: thesis: a,b,c,s are_coplanar

now :: thesis: ( not a,b,c are_collinear implies a,b,c,s are_coplanar )

b,b,a are_collinear by ANPROJ_2:def 7;
then A6: b,a,c,b are_coplanar by Th6;
A7: b,a,c,r are_coplanar by A3, Th7;
assume A8: not a,b,c are_collinear ; :: thesis: a,b,c,s are_coplanar
then A9: not b,a,c are_collinear by Th1;
a,p,q,r are_coplanar by A2, A3, A4, A8, Lm5;
then A10: p,q,r,a are_coplanar by Th7;
A11: c,a,b,r are_coplanar by A3, Th7;
A12: not c,a,b are_collinear by A8, Th1;
( c,a,b,p are_coplanar & c,a,b,q are_coplanar ) by A2, A4, Th7;
then c,p,q,r are_coplanar by A12, A11, Lm5;
then A13: p,q,r,c are_coplanar by Th7;
( b,a,c,p are_coplanar & b,a,c,q are_coplanar ) by A2, A4, Th7;
then p,q,r,b are_coplanar by A9, A6, A7, Th8;
hence a,b,c,s are_coplanar by A1, A5, A10, A13, Th8; :: thesis: verum

end;

hence a,b,c,s are_coplanar by Th6; :: thesis: verum