const Eps_i : (set prop) set term Descr_ii = \P:(set set) prop.\x:set.Eps_i \y:set.!f:set set.P f -> f x = y axiom func_ext: !f:set set.!f2:set set.(!x:set.f x = f2 x) -> f = f2 lemma !P:(set set) prop.!f:set set.(!f2:set set.!f3:set set.P f2 -> P f3 -> f2 = f3) -> P f -> f = Descr_ii P -> P (Descr_ii P) lemma !P:(set set) prop.!f:set set.!x:set.(!f2:set set.!f3:set set.P f2 -> P f3 -> f2 = f3) -> P f -> (!f2:set set.P f2 -> f2 x = f x) -> f x = Descr_ii P x claim !P:(set set) prop.(?f:set set.P f) -> (!f:set set.!f2:set set.P f -> P f2 -> f = f2) -> P (Descr_ii P)