const In : set set prop term iIn = In infix iIn 2000 2000 const Union : set set term Union_closed = \x:set.!y:set.y iIn x -> Union y iIn x const ZF_closed : set prop const Power_closed : set prop const Repl_closed : set prop axiom ZF_closed_E: !x:set.ZF_closed x -> !P:prop.(Union_closed x -> Power_closed x -> Repl_closed x -> P) -> P claim !x:set.ZF_closed x -> !y:set.y iIn x -> Union y iIn x