const In : set set prop term iIn = In infix iIn 2000 2000 const ordsucc : set set axiom ordsuccI2: !x:set.x iIn ordsucc x const SNo : set prop const SNoLev : set set const SNo_extend1 : set set axiom SNo_extend1_SNoLev: !x:set.SNo x -> SNoLev (SNo_extend1 x) = ordsucc (SNoLev x) const binintersect : set set set const SNoElts_ : set set lemma !x:set.SNo x -> SNo (SNo_extend1 x) -> SNoLev x iIn SNoLev (SNo_extend1 x) -> x = binintersect (SNo_extend1 x) (SNoElts_ (SNoLev x)) var x:set hyp SNo x claim SNo (SNo_extend1 x) -> x = binintersect (SNo_extend1 x) (SNoElts_ (SNoLev x))