const Descr_Vo1 : ((set prop) prop) set prop const Eps_i : (set prop) set term DescrR_i_io_1 = \P:set (set prop) prop.Eps_i \x:set.(?p:set prop.P x p) & !p:set prop.!q:set prop.P x p -> P x q -> p = q term DescrR_i_io_2 = \P:set (set prop) prop.Descr_Vo1 (P (DescrR_i_io_1 P)) axiom Eps_i_ex: !p:set prop.(?x:set.p x) -> p (Eps_i p) lemma !P:set (set prop) prop.(?x:set.(?p:set prop.P x p) & !p:set prop.!q:set prop.P x p -> P x q -> p = q) -> (?p:set prop.P (DescrR_i_io_1 P) p) & (!p:set prop.!q:set prop.P (DescrR_i_io_1 P) p -> P (DescrR_i_io_1 P) q -> p = q) -> P (DescrR_i_io_1 P) (DescrR_i_io_2 P) claim !P:set (set prop) prop.(?x:set.(?p:set prop.P x p) & !p:set prop.!q:set prop.P x p -> P x q -> p = q) -> P (DescrR_i_io_1 P) (DescrR_i_io_2 P)