let PCPP be CollProjectiveSpace; :: thesis: for p being Element of PCPP holds
not for q, r being Element of PCPP holds p,q,r are_collinear
let p be Element of PCPP; :: thesis: not for q, r being Element of PCPP holds p,q,r are_collinear
consider q being Element of PCPP 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 PCPP holds p,q,r are_collinear by A1, Th4;
hence not for q, r being Element of PCPP holds p,q,r are_collinear ; :: thesis: verum