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