1\THEOREM DECOMPOSITION pred_sets 2|- !s x. x IN s = (?t. (s = x INSERT t) /\ ~x IN t) 3\ENDTHEOREM 4