theorem Th1: :: COLLSP:1

for X being set holds
( X = {} or ex a being set st
( {a} = X or ex a, b being set st
( a <> b & a in X & b in X ) ) )