const In : set set prop term iIn = In infix iIn 2000 2000 term Subq = \x:set.\y:set.!z:set.z iIn x -> z iIn y term nIn = \x:set.\y:set.~ x iIn y axiom FalseE: ~ False const binunion : set set set axiom binunionE: !x:set.!y:set.!z:set.z iIn binunion x y -> z iIn x | z iIn y const setminus : set set set axiom setminusE: !x:set.!y:set.!z:set.z iIn setminus x y -> z iIn x & nIn z y const finite : set prop const Sing : set set axiom adjoin_finite: !x:set.!y:set.finite x -> finite (binunion x (Sing y)) var x:set var y:set var z:set hyp !w:set.Subq w x -> finite w hyp Subq z (binunion x (Sing y)) hyp y iIn z claim z = binunion (setminus z (Sing y)) (Sing y) -> finite z