const SNo : set prop const In : set set prop term iIn = In infix iIn 2000 2000 const SNoLev : set set const SNo_ : set set prop const binintersect : set set set const SNoElts_ : set set axiom restr_SNo_: !x:set.SNo x -> !y:set.y iIn SNoLev x -> SNo_ y (binintersect x (SNoElts_ y)) const ordinal : set prop lemma !x:set.!y:set.SNo x -> y iIn SNoLev x -> ordinal y -> SNo_ y (binintersect x (SNoElts_ y)) -> SNo (binintersect x (SNoElts_ y)) var x:set var y:set hyp SNo x hyp y iIn SNoLev x claim ordinal y -> SNo (binintersect x (SNoElts_ y))