1\THEOREM INSERT_SUBSET pred_sets 2|- !x s t. (x INSERT s) SUBSET t = x IN t /\ s SUBSET t 3\ENDTHEOREM 4