1\THEOREM IN_DELETE_EQ pred_sets
2|- !s x x'.
3    (x IN s = x' IN s) = (x IN (s DELETE x') = x' IN (s DELETE x))
4\ENDTHEOREM
5