let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for a, b, c, p, q being Element of FCPS st not a,b,c is_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar holds
a,b,p,q are_coplanar
let a, b, c, p, q be Element of FCPS; :: thesis: ( not a,b,c is_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar implies a,b,p,q are_coplanar )
assume that
A1: not a,b,c is_collinear and
A2: a,b,c,p are_coplanar and
A3: a,b,c,q are_coplanar ; :: thesis: a,b,p,q are_coplanar
consider x being Element of FCPS such that
A4: a,b,x is_collinear and
A5: c,p,x is_collinear by A2, Def1;
consider y being Element of FCPS such that
A6: a,b,y is_collinear and
A7: c,q,y is_collinear by A3, Def1;

A8: now

assume A9: a <> b ; :: thesis: a,b,p,q are_coplanar
( b,a,x is_collinear & b,a,y is_collinear ) by A4, A6, Th1;
then b,x,y is_collinear by A9, COLLSP:6;
then A10: x,y,b is_collinear by Th1;
a,x,y is_collinear by A4, A6, A9, COLLSP:6;
then A11: x,y,a is_collinear by Th1;

A12: now

p,c,x is_collinear by A5, Th1;
then consider z being Element of FCPS such that
A13: p,q,z is_collinear and
A14: x,y,z is_collinear by A7, ANPROJ_2:def 9;
assume x <> y ; :: thesis: a,b,p,q are_coplanar
then a,b,z is_collinear by A11, A10, A14, ANPROJ_2:def 8;
hence a,b,p,q are_coplanar by A13, Def1; :: thesis: verum

end;

now

assume x = y ; :: thesis: a,b,p,q are_coplanar
then A15: x,c,q is_collinear by A7, Th1;
x,c,p is_collinear by A5, Th1;
then x,p,q is_collinear by A1, A4, A15, COLLSP:6;
then p,q,x is_collinear by Th1;
hence a,b,p,q are_coplanar by A4, Def1; :: thesis: verum

end;

hence a,b,p,q are_coplanar by A12; :: thesis: verum

end;

now

assume a = b ; :: thesis: a,b,p,q are_coplanar
then a,b,p is_collinear by ANPROJ_2:def 7;
hence a,b,p,q are_coplanar by Th10; :: thesis: verum

end;

hence a,b,p,q are_coplanar by A8; :: thesis: verum