let PCPP be CollProjectiveSpace; :: thesis: for p, q being Element of PCPP st p <> q holds
ex r being Element of PCPP st not p,q,r is_collinear
let p, q be Element of PCPP; :: thesis: ( p <> q implies ex r being Element of PCPP st not p,q,r is_collinear )
assume A1: p <> q ; :: thesis: not for r being Element of PCPP holds p,q,r is_collinear
consider a, b, c being Element of PCPP such that
A2: not a,b,c is_collinear by COLLSP:def 6;
( p,q,a is_collinear & p,q,b is_collinear implies not p,q,c is_collinear ) by A1, A2, ANPROJ_2:def 8;
hence not for r being Element of PCPP holds p,q,r is_collinear ; :: thesis: verum