const ordinal : set prop const PNoLe : set (set prop) set (set prop) prop term PNo_upc = \P:set (set prop) prop.\x:set.\p:set prop.?y:set.ordinal y & ?q:set prop.P y q & PNoLe y q x p 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 y q x p