1\THEOREM INSERT_INTER pred_sets
2|- !x s t.
3    (x INSERT s) INTER t = (x IN t => x INSERT (s INTER t) | s INTER t)
4\ENDTHEOREM
5