const ordinal : set prop const PNoLe : set (set prop) set (set prop) prop term PNo_downc = \P:set (set prop) prop.\x:set.\p:set prop.?y:set.ordinal y & ?q:set prop.P y q & PNoLe x p y q axiom PNoLe_ref: !x:set.!p:set prop.PNoLe x p x p claim !P:set (set prop) prop.!x:set.ordinal x -> !p:set prop.P x p -> ?y:set.ordinal y & ?q:set prop.P y q & PNoLe x p y q