let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for p, q, r being Element of FCPS st not p,q,r is_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 is_collinear implies ex s being Element of FCPS st not p,q,r,s are_coplanar )
assume A1: not p,q,r is_collinear ; :: thesis: not for s being Element of FCPS holds p,q,r,s are_coplanar
assume A2: for s being Element of FCPS holds p,q,r,s are_coplanar ; :: thesis: contradiction
consider a, b, c, d being Element of FCPS such that
A3: not a,b,c,d are_coplanar by Th16;
( p,q,r,a are_coplanar & p,q,r,b are_coplanar & p,q,r,c are_coplanar & p,q,r,d are_coplanar ) by A2;
hence contradiction by A1, A3, Th12; :: thesis: verum