1\THEOREM DELETE_DELETE pred_sets
2|- !x s. (s DELETE x) DELETE x = s DELETE x
3\ENDTHEOREM
4