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 A1: ( not a,b,c is_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar ) ; :: thesis: a,b,p,q are_coplanar
then consider x being Element of FCPS such that
A2: ( a,b,x is_collinear & c,p,x is_collinear ) by Def1;
consider y being Element of FCPS such that
A3: ( a,b,y is_collinear & c,q,y is_collinear ) by A1, Def1;

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

now

assume A5: a <> b ; :: thesis: a,b,p,q are_coplanar
then A6: a,x,y is_collinear by A2, A3, COLLSP:11;
( b,a,x is_collinear & b,a,y is_collinear ) by A2, A3, Th1;
then b,x,y is_collinear by A5, COLLSP:11;
then A7: ( x,y,a is_collinear & x,y,b is_collinear ) by A6, Th1;

A8: now

assume x = y ; :: thesis: a,b,p,q are_coplanar
then ( x,c,p is_collinear & x,c,q is_collinear ) by A2, A3, Th1;
then x,p,q is_collinear by A1, A2, COLLSP:11;
then p,q,x is_collinear by Th1;
hence a,b,p,q are_coplanar by A2, Def1; :: thesis: verum

end;

now

assume A9: x <> y ; :: thesis: a,b,p,q are_coplanar
( p,c,x is_collinear & c,q,y is_collinear ) by A2, A3, Th1;
then consider z being Element of FCPS such that
A10: ( p,q,z is_collinear & x,y,z is_collinear ) by ANPROJ_2:def 9;
a,b,z is_collinear by A7, A9, A10, ANPROJ_2:def 8;
hence a,b,p,q are_coplanar by A10, Def1; :: thesis: verum

end;

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

end;

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