let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for p being Element of FCPS holds

not for q, r being Element of FCPS holds p,q,r are_collinear

let p be Element of FCPS; :: thesis: not for q, r being Element of FCPS holds p,q,r are_collinear

consider q being Element of FCPS such that

A1: p <> q and

p <> q and

p,p,q are_collinear by ANPROJ_2:def 10;

not for r being Element of FCPS holds p,q,r are_collinear by A1, COLLSP:12;

hence not for q, r being Element of FCPS holds p,q,r are_collinear ; :: thesis: verum

not for q, r being Element of FCPS holds p,q,r are_collinear

let p be Element of FCPS; :: thesis: not for q, r being Element of FCPS holds p,q,r are_collinear

consider q being Element of FCPS such that

A1: p <> q and

p <> q and

p,p,q are_collinear by ANPROJ_2:def 10;

not for r being Element of FCPS holds p,q,r are_collinear by A1, COLLSP:12;

hence not for q, r being Element of FCPS holds p,q,r are_collinear ; :: thesis: verum