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