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