const In : set set prop term iIn = In infix iIn 2000 2000 term Subq = \x:set.\y:set.!z:set.z iIn x -> z iIn y const ordinal : set prop const PNo_strict_imv : (set (set prop) prop) (set (set prop) prop) set (set prop) prop term PNo_least_rep = \P:set (set prop) prop.\Q:set (set prop) prop.\x:set.\p:set prop.ordinal x & PNo_strict_imv P Q x p & !y:set.y iIn x -> !q:set prop.~ PNo_strict_imv P Q y q const ordsucc : set set const PNo_bd : (set (set prop) prop) (set (set prop) prop) set var P:set (set prop) prop var Q:set (set prop) prop var x:set var y:set var p:set prop hyp !z:set.z iIn PNo_bd P Q -> !q:set prop.~ PNo_strict_imv P Q z q hyp y iIn ordsucc x hyp PNo_strict_imv P Q y p hyp Subq (ordsucc x) (PNo_bd P Q) claim ~ y iIn PNo_bd P Q