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