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