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 const finite : set prop const Empty : set axiom finite_Empty: finite Empty axiom Empty_Subq_eq: !x:set.Subq x Empty -> x = Empty const binunion : set set set axiom binunionI2: !x:set.!y:set.!z:set.z iIn y -> z iIn binunion x y const setminus : set set set axiom setminusI: !x:set.!y:set.!z:set.z iIn x -> nIn z y -> z iIn setminus x y axiom binunionI1: !x:set.!y:set.!z:set.z iIn x -> z iIn binunion x y axiom xm: !P:prop.P | ~ P axiom setminusE1: !x:set.!y:set.!z:set.z iIn setminus x y -> z iIn x const Sing : set set axiom SingE: !x:set.!y:set.y iIn Sing x -> y = x axiom binunionE: !x:set.!y:set.!z:set.z iIn binunion x y -> z iIn x | z iIn y axiom set_ext: !x:set.!y:set.Subq x y -> Subq y x -> x = y axiom FalseE: ~ False axiom finite_ind: !p:set prop.p Empty -> (!x:set.!y:set.finite x -> nIn y x -> p x -> p (binunion x (Sing y))) -> !x:set.finite x -> p x lemma !x:set.!y:set.!z:set.(!w:set.Subq w x -> finite w) -> Subq z (binunion x (Sing y)) -> y iIn z -> z = binunion (setminus z (Sing y)) (Sing y) -> finite z claim !x:set.finite x -> !y:set.Subq y x -> finite y