const Eps_i : (set prop) set term Descr_iii = \P:(set set set) prop.\x:set.\y:set.Eps_i \z:set.!g:set set set.P g -> g x y = z axiom Eps_i_ax: !p:set prop.!x:set.p x -> p (Eps_i p) lemma !P:(set set set) prop.!g:set set set.!x:set.!y:set.P g -> (!h:set set set.P h -> h x y = g x y) -> (!h:set set set.P h -> h x y = Descr_iii P x y) -> g x y = Descr_iii P x y var P:(set set set) prop var g:set set set var x:set var y:set hyp !h:set set set.!g2:set set set.P h -> P g2 -> h = g2 hyp P g claim (!h:set set set.P h -> h x y = g x y) -> g x y = Descr_iii P x y