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