1\THEOREM SUBSET_INSERT_DELETE pred_sets 2|- !x s t. s SUBSET (x INSERT t) = (s DELETE x) SUBSET t 3\ENDTHEOREM 4