const Eps_i : (set prop) set axiom Eps_i_ax: !p:set prop.!x:set.p x -> p (Eps_i p) claim !p:set prop.(?x:set.p x) -> p (Eps_i p)