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