let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for p, q, r being Element of FCPS st not p,q,r are_collinear holds

ex s being Element of FCPS st not p,q,r,s are_coplanar

let p, q, r be Element of FCPS; :: thesis: ( not p,q,r are_collinear implies ex s being Element of FCPS st not p,q,r,s are_coplanar )

assume A1: not p,q,r are_collinear ; :: thesis: not for s being Element of FCPS holds p,q,r,s are_coplanar

consider a, b, c, d being Element of FCPS such that

A2: not a,b,c,d are_coplanar by Th12;

assume A3: for s being Element of FCPS holds p,q,r,s are_coplanar ; :: thesis: contradiction

then A4: ( p,q,r,c are_coplanar & p,q,r,d are_coplanar ) ;

( p,q,r,a are_coplanar & p,q,r,b are_coplanar ) by A3;

hence contradiction by A1, A2, A4, Th8; :: thesis: verum

ex s being Element of FCPS st not p,q,r,s are_coplanar

let p, q, r be Element of FCPS; :: thesis: ( not p,q,r are_collinear implies ex s being Element of FCPS st not p,q,r,s are_coplanar )

assume A1: not p,q,r are_collinear ; :: thesis: not for s being Element of FCPS holds p,q,r,s are_coplanar

consider a, b, c, d being Element of FCPS such that

A2: not a,b,c,d are_coplanar by Th12;

assume A3: for s being Element of FCPS holds p,q,r,s are_coplanar ; :: thesis: contradiction

then A4: ( p,q,r,c are_coplanar & p,q,r,d are_coplanar ) ;

( p,q,r,a are_coplanar & p,q,r,b are_coplanar ) by A3;

hence contradiction by A1, A2, A4, Th8; :: thesis: verum