const Union_closed : set prop const Power_closed : set prop const Repl_closed : set prop term ZF_closed = \x:set.Union_closed x & Power_closed x & Repl_closed x claim !x:set.ZF_closed x -> !P:prop.(Union_closed x -> Power_closed x -> Repl_closed x -> P) -> P