1\THEOREM SUBSET_INSERT pred_sets 2|- !x s. ~x IN s ==> (!t. s SUBSET (x INSERT t) = s SUBSET t) 3\ENDTHEOREM 4