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