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;

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;

end;( 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;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

now :: thesis: ( x = y implies a,b,p,q are_coplanar )

hence
a,b,p,q are_coplanar
by A12; :: thesis: verumassume
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;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

now :: thesis: ( a = b implies a,b,p,q are_coplanar )

hence
a,b,p,q are_coplanar
by A8; :: thesis: verumassume
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;then a,b,p are_collinear by ANPROJ_2:def 7;

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