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 is_collinear
let p be Element of FCPS; :: thesis: not for q, r being Element of FCPS holds p,q,r is_collinear
consider q being Element of FCPS such that
A1: ( p <> q & p <> q & p,p,q is_collinear ) by ANPROJ_2:def 10;
not for r being Element of FCPS holds p,q,r is_collinear by A1, COLLSP:19;
hence not for q, r being Element of FCPS holds p,q,r is_collinear ; :: thesis: verum