const In : set set prop term iIn = In infix iIn 2000 2000 term Subq = \x:set.\y:set.!z:set.z iIn x -> z iIn y term nIn = \x:set.\y:set.~ x iIn y const SNoL : set set const SNoS_ : set set const SNoLev : set set axiom SNoL_SNoS_: !x:set.Subq (SNoL x) (SNoS_ (SNoLev x)) const Empty : set axiom SNoLev_0: SNoLev Empty = Empty axiom Empty_Subq_eq: !x:set.Subq x Empty -> x = Empty lemma !x:set.x iIn SNoL Empty -> x iIn SNoS_ Empty -> x iIn Empty claim SNoL Empty = Empty