const PNo_rel_strict_imv : (set (set prop) prop) (set (set prop) prop) set (set prop) prop const ordsucc : set set term PNo_rel_strict_split_imv = \P:set (set prop) prop.\Q:set (set prop) prop.\x:set.\p:set prop.PNo_rel_strict_imv P Q (ordsucc x) (\y:set.p y & y != x) & PNo_rel_strict_imv P Q (ordsucc x) \y:set.p y | y = x const ordinal : set prop const PNo_lenbdd : set (set (set prop) prop) prop axiom PNo_lenbdd_strict_imv_extend0: !P:set (set prop) prop.!Q:set (set prop) prop.!x:set.ordinal x -> PNo_lenbdd x P -> PNo_lenbdd x Q -> !p:set prop.PNo_rel_strict_imv P Q x p -> PNo_rel_strict_imv P Q (ordsucc x) \y:set.p y & y != x axiom PNo_lenbdd_strict_imv_extend1: !P:set (set prop) prop.!Q:set (set prop) prop.!x:set.ordinal x -> PNo_lenbdd x P -> PNo_lenbdd x Q -> !p:set prop.PNo_rel_strict_imv P Q x p -> PNo_rel_strict_imv P Q (ordsucc x) \y:set.p y | y = x claim !P:set (set prop) prop.!Q:set (set prop) prop.!x:set.ordinal x -> PNo_lenbdd x P -> PNo_lenbdd x Q -> !p:set prop.PNo_rel_strict_imv P Q x p -> PNo_rel_strict_imv P Q (ordsucc x) (\y:set.p y & y != x) & PNo_rel_strict_imv P Q (ordsucc x) \y:set.p y | y = x