const In : set set prop term iIn = In infix iIn 2000 2000 const omega : set const equip : set set prop term finite = \x:set.?y:set.y iIn omega & equip x y term Subq = \x:set.\y:set.!z:set.z iIn x -> z iIn y term TransSet = \x:set.!y:set.y iIn x -> Subq y x const ordinal : set prop axiom omega_ordinal: ordinal omega axiom omega_TransSet: TransSet omega const SNoS_ : set set axiom SNoS_Subq: !x:set.!y:set.ordinal x -> ordinal y -> Subq x y -> Subq (SNoS_ x) (SNoS_ y) const Sep : set (set prop) set axiom SepI: !x:set.!p:set prop.!y:set.y iIn x -> p y -> y iIn Sep x p const famunion : set (set set) set axiom famunionI: !x:set.!f:set set.!y:set.!z:set.y iIn x -> z iIn f y -> z iIn famunion x f const SNoLev : set set const SNo : set prop const SNo_ : set set prop axiom SNoS_E2: !x:set.ordinal x -> !y:set.y iIn SNoS_ x -> !P:prop.(SNoLev y iIn x -> ordinal (SNoLev y) -> SNo y -> SNo_ (SNoLev y) y -> P) -> P axiom SNoS_I: !x:set.ordinal x -> !y:set.!z:set.z iIn x -> SNo_ z y -> y iIn SNoS_ x axiom SepE: !x:set.!p:set prop.!y:set.y iIn Sep x p -> y iIn x & p y axiom famunionE_impred: !x:set.!f:set set.!y:set.y iIn famunion x f -> !P:prop.(!z:set.z iIn x -> y iIn f z -> P) -> P axiom set_ext: !x:set.!y:set.Subq x y -> Subq y x -> x = y const nat_p : set prop lemma !x:set.x iIn omega -> nat_p x -> ordinal x -> SNoS_ x = famunion x (\y:set.Sep (SNoS_ omega) \z:set.SNoLev z = y) -> finite (SNoS_ x) var x:set hyp x iIn omega hyp nat_p x claim ordinal x -> finite (SNoS_ x)