const ordinal : set prop const SNo_ : set set prop const SNoLev : set set axiom SNoLev_uniq2: !x:set.ordinal x -> !y:set.SNo_ x y -> SNoLev y = x const In : set set prop term iIn = In infix iIn 2000 2000 const SNo : set prop 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)) -> SNoLev (binintersect x (SNoElts_ y)) = y