let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for a, b, c, p, q being Element of FCPS st not a,b,c are_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 are_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 are_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 are_collinear and
A5: c,p,x are_collinear by A2;
consider y being Element of FCPS such that
A6: a,b,y are_collinear and
A7: c,q,y are_collinear by A3;
A8: now :: thesis: ( a <> b implies a,b,p,q are_coplanar )
assume A9: a <> b ; :: thesis: a,b,p,q are_coplanar
( b,a,x are_collinear & b,a,y are_collinear ) by A4, A6, Th1;
then b,x,y are_collinear by A9, COLLSP:6;
then A10: x,y,b are_collinear by Th1;
a,x,y are_collinear by A4, A6, A9, COLLSP:6;
then A11: x,y,a are_collinear by Th1;
A12: now :: thesis: ( x <> y implies a,b,p,q are_coplanar )
p,c,x are_collinear by A5, Th1;
then consider z being Element of FCPS such that
A13: p,q,z are_collinear and
A14: x,y,z are_collinear by A7, ANPROJ_2:def 9;
assume x <> y ; :: thesis: a,b,p,q are_coplanar
then a,b,z are_collinear by A11, A10, A14, ANPROJ_2:def 8;
hence a,b,p,q are_coplanar by A13; :: thesis: verum
end;
now :: thesis: ( x = y implies a,b,p,q are_coplanar )
assume x = y ; :: thesis: a,b,p,q are_coplanar
then A15: x,c,q are_collinear by A7, Th1;
x,c,p are_collinear by A5, Th1;
then x,p,q are_collinear by A1, A4, A15, COLLSP:6;
then p,q,x are_collinear by Th1;
hence a,b,p,q are_coplanar by A4; :: thesis: verum
end;
hence a,b,p,q are_coplanar by A12; :: thesis: verum
end;
now :: thesis: ( a = b implies a,b,p,q are_coplanar )
assume a = b ; :: thesis: a,b,p,q are_coplanar
then a,b,p are_collinear by ANPROJ_2:def 7;
hence a,b,p,q are_coplanar by Th6; :: thesis: verum
end;
hence a,b,p,q are_coplanar by A8; :: thesis: verum