let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for a, b, c, p, q, r, s being Element of FCPS st not a,b,c is_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar & a,b,c,r are_coplanar & a,b,c,s are_coplanar holds
ex x being Element of FCPS st
( p,q,x is_collinear & r,s,x is_collinear )
let a, b, c, p, q, r, s be Element of FCPS; :: thesis: ( not a,b,c is_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar & a,b,c,r are_coplanar & a,b,c,s are_coplanar implies ex x being Element of FCPS st
( p,q,x is_collinear & r,s,x is_collinear ) )
assume ( not a,b,c is_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar & a,b,c,r are_coplanar & a,b,c,s are_coplanar ) ; :: thesis: ex x being Element of FCPS st
( p,q,x is_collinear & r,s,x is_collinear )
then p,q,r,s are_coplanar by Th12;
then consider x being Element of FCPS such that
A1: ( p,q,x is_collinear & r,s,x is_collinear ) by Def1;
take x ; :: thesis: ( p,q,x is_collinear & r,s,x is_collinear )
thus ( p,q,x is_collinear & r,s,x is_collinear ) by A1; :: thesis: verum