1\THEOREM DELETE_COMM pred_sets 2|- !x y s. (s DELETE x) DELETE y = (s DELETE y) DELETE x 3\ENDTHEOREM 4