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