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