1\THEOREM EMPTY_DELETE pred_sets
2|- !x. {{}} DELETE x = {{}}
3\ENDTHEOREM
4