const PNo_least_rep : (set (set prop) prop) (set (set prop) prop) set (set prop) prop const nIn : set set prop term PNo_least_rep2 = \P:set (set prop) prop.\Q:set (set prop) prop.\x:set.\p:set prop.PNo_least_rep P Q x p & !y:set.nIn y x -> ~ p y 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 const PNo_bd : (set (set prop) prop) (set (set prop) prop) set const PNo_pred : (set (set prop) prop) (set (set prop) prop) set prop axiom PNo_bd_pred_lem: !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) 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_rep P Q (PNo_bd P Q) (PNo_pred P Q)