const DescrR_i_io_2 : (set (set prop) prop) set prop const PNo_least_rep2 : (set (set prop) prop) (set (set prop) prop) set (set prop) prop term PNo_pred = \P:set (set prop) prop.\Q:set (set prop) prop.DescrR_i_io_2 (PNo_least_rep2 P Q) const DescrR_i_io_1 : (set (set prop) prop) set term PNo_bd = \P:set (set prop) prop.\Q:set (set prop) prop.DescrR_i_io_1 (PNo_least_rep2 P Q) const PNoLt_pwise : (set (set prop) prop) (set (set prop) prop) prop const ordinal : set prop const PNo_lenbdd : set (set (set prop) prop) prop axiom PNo_lenbdd_least_rep2_exuniq2: !P:set (set prop) prop.!Q:set (set prop) prop.PNoLt_pwise P Q -> !x:set.ordinal x -> PNo_lenbdd x P -> PNo_lenbdd x Q -> ?y:set.(?p:set prop.PNo_least_rep2 P Q y p) & !p:set prop.!q:set prop.PNo_least_rep2 P Q y p -> PNo_least_rep2 P Q y q -> p = q axiom DescrR_i_io_12: !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) claim !P:set (set prop) prop.!Q:set (set prop) prop.PNoLt_pwise P Q -> !x:set.ordinal x -> PNo_lenbdd x P -> PNo_lenbdd x Q -> PNo_least_rep2 P Q (PNo_bd P Q) (PNo_pred P Q)