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