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