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