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 func_ext: !f:set set.!f2:set set.(!x:set.f x = f2 x) -> f = f2 lemma !P:(set set set) prop.!g:set set set.(!h:set set set.!g2:set set set.P h -> P g2 -> h = g2) -> P g -> g = Descr_iii P -> P (Descr_iii P) lemma !P:(set set set) prop.!g:set set set.!x:set.!y:set.(!h:set set set.!g2:set set set.P h -> P g2 -> h = g2) -> P g -> (!h:set set set.P h -> h x y = g x y) -> g x y = Descr_iii P x y claim !P:(set set set) prop.(?g:set set set.P g) -> (!g:set set set.!h:set set set.P g -> P h -> g = h) -> P (Descr_iii P)