const In : set set prop term iIn = In infix iIn 2000 2000 const Power : set set term Power_closed = \x:set.!y:set.y iIn x -> Power y iIn x const ZF_closed : set prop const Union_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 -> Power y iIn x