const binunion : set set set const Sing : set set term ordsucc = \x:set.binunion x (Sing x) const ZF_closed : set prop const In : set set prop term iIn = In infix iIn 2000 2000 axiom ZF_Sing_closed: !x:set.ZF_closed x -> !y:set.y iIn x -> Sing y iIn x axiom ZF_binunion_closed: !x:set.ZF_closed x -> !y:set.y iIn x -> !z:set.z iIn x -> binunion y z iIn x claim !x:set.ZF_closed x -> !y:set.y iIn x -> ordsucc y iIn x