const Eps_i : (set prop) set const In_rec_i_G : (set (set set) set) set set prop term In_rec_i = \P:set (set set) set.\x:set.Eps_i (In_rec_i_G P x) const In : set set prop term iIn = In infix iIn 2000 2000 axiom In_rec_i_G_c: !P:set (set set) set.!x:set.!f:set set.(!y:set.y iIn x -> In_rec_i_G P y (f y)) -> In_rec_i_G P x (P x f) axiom Eps_i_ax: !p:set prop.!x:set.p x -> p (Eps_i p) axiom In_ind: !p:set prop.(!x:set.(!y:set.y iIn x -> p y) -> p x) -> !x:set.p x claim !P:set (set set) set.(!x:set.!f:set set.!f2:set set.(!y:set.y iIn x -> f y = f2 y) -> P x f = P x f2) -> !x:set.In_rec_i_G P x (In_rec_i P x)