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_tra: !x:set.!y:set.!z:set.ordinal x -> ordinal y -> ordinal z -> !p:set prop.!q:set prop.!p2:set prop.PNoLe x p y q -> PNoLe y q z p2 -> PNoLe x p z p2 claim !P:set (set prop) prop.!x:set.!y:set.!p:set prop.!q:set prop.ordinal x -> ordinal y -> PNo_upc P x p -> PNoLe x p y q -> ?z:set.ordinal z & ?p2:set prop.P z p2 & PNoLe z p2 y q