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