const Sep : set (set prop) set const Power : set set const SNoElts_ : set set const In : set set prop term iIn = In infix iIn 2000 2000 const SNo_ : set set prop term SNoS_ = \x:set.Sep (Power (SNoElts_ x)) \y:set.?z:set.z iIn x & SNo_ z y axiom SepE2: !x:set.!p:set prop.!y:set.y iIn Sep x p -> p y const ordinal : set prop claim !x:set.ordinal x -> !y:set.y iIn SNoS_ x -> ?z:set.z iIn x & SNo_ z y