1\THEOREM SUBSET_DELETE pred_sets 2|- !x s t. s SUBSET (t DELETE x) = ~x IN s /\ s SUBSET t 3\ENDTHEOREM 4