let CPS be proper CollSp; ex a9, b9, c9 being Point of CPS st
( a9 <> b9 & b9 <> c9 & c9 <> a9 )
consider a99, b99, c99 being Point of CPS such that
A1:
not a99,b99,c99 are_collinear
by COLLSP:def 6;
A2:
c99 <> a99
by A1, COLLSP:2;
( a99 <> b99 & b99 <> c99 )
by A1, COLLSP:2;
hence
ex a9, b9, c9 being Point of CPS st
( a9 <> b9 & b9 <> c9 & c9 <> a9 )
by A2; verum