const PNoLt : set (set prop) set (set prop) prop const PNoEq_ : set (set prop) (set prop) prop term PNoLe = \x:set.\p:set prop.\y:set.\q:set prop.PNoLt x p y q | x = y & PNoEq_ x p q const ordinal : set prop term PNoLt_pwise = \P:set (set prop) prop.\Q:set (set prop) prop.!x:set.ordinal x -> !p:set prop.P x p -> !y:set.ordinal y -> !q:set prop.Q y q -> PNoLt x p y q 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 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 PNoLtLe_tra: !x:set.!y:set.!z:set.ordinal x -> ordinal y -> ordinal z -> !p:set prop.!q:set prop.!p2:set prop.PNoLt x p y q -> PNoLe y q z p2 -> PNoLt x p z p2 axiom PNoLeLt_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 -> PNoLt y q z p2 -> PNoLt x p z p2 lemma !P:set (set prop) prop.!Q:set (set prop) prop.!x:set.!p:set prop.!y:set.!q:set prop.!z:set.!p2:set prop.!w:set.!q2:set prop.PNoLt_pwise P Q -> ordinal x -> ordinal y -> ordinal z -> P z p2 -> PNoLe x p z p2 -> ordinal w -> Q w q2 -> PNoLe w q2 y q -> PNoLt x p y q -> PNoLt x p y q claim !P:set (set prop) prop.!Q:set (set prop) prop.PNoLt_pwise P Q -> !x:set.ordinal x -> !p:set prop.PNo_downc P x p -> !y:set.ordinal y -> !q:set prop.PNo_upc Q y q -> PNoLt x p y q