consider a, b, c being Point of CLSP such that
A1:
not a,b,c are_collinear
by Def6;
take
Line (a,b)
; ex a, b being Point of CLSP st
( a <> b & Line (a,b) = Line (a,b) )
a <> b
by A1, Th2;
hence
ex a, b being Point of CLSP st
( a <> b & Line (a,b) = Line (a,b) )
; verum