let CLSP be proper CollSp; :: thesis: for p, q being Point of CLSP st p <> q holds
ex r being Point of CLSP st not p,q,r is_collinear
let p, q be Point of CLSP; :: thesis: ( p <> q implies ex r being Point of CLSP st not p,q,r is_collinear )
consider a, b, c being Point of CLSP such that
A1: not a,b,c is_collinear by Def6;
assume p <> q ; :: thesis: not for r being Point of CLSP holds p,q,r is_collinear
then ( not p,q,a is_collinear or not p,q,b is_collinear or not p,q,c is_collinear ) by A1, Th8;
hence not for r being Point of CLSP holds p,q,r is_collinear ; :: thesis: verum