let FCPS be up-3-dimensional CollProjectiveSpace; 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; 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
; verum