let CPS be proper CollSp; :: thesis: 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; :: thesis: verum