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 axiom FalseE: ~ False axiom ordinal_In_Or_Subq: !x:set.!y:set.ordinal x -> ordinal y -> x iIn y | Subq y x const PNo_bd : (set (set prop) prop) (set (set prop) prop) set const ordsucc : set set lemma !P:set (set prop) prop.!Q:set (set prop) prop.!x:set.!y:set.!p:set prop.(!z:set.z iIn PNo_bd P Q -> !q:set prop.~ PNo_strict_imv P Q z q) -> y iIn ordsucc x -> PNo_strict_imv P Q y p -> Subq (ordsucc x) (PNo_bd P Q) -> ~ y iIn PNo_bd P Q var P:set (set prop) prop var Q:set (set prop) prop var x:set var y:set var p:set prop hyp ordinal x hyp ordinal (PNo_bd P Q) 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 claim ordinal (ordsucc x) -> PNo_bd P Q iIn ordsucc x