let CPS be proper CollSp; :: thesis: ex a', b', c' being Point of CPS st
( a' <> b' & b' <> c' & c' <> a' )
consider a'', b'', c'' being Point of CPS such that
A1: not a'',b'',c'' is_collinear by COLLSP:def 6;
( a'' <> b'' & b'' <> c'' & c'' <> a'' ) by A1, COLLSP:7;
hence ex a', b', c' being Point of CPS st
( a' <> b' & b' <> c' & c' <> a' ) ; :: thesis: verum