enrich
   nat
with
   sorts iset('a);
   constants 
       ∅ : iset('a);
   
   functions 
       . ++ . : iset('a) × 'a → iset('a) prio 9 left;
       χ : iset('a) → 'a → bool;
       { . } : ('a → bool) → iset('a);
   
   predicates 
       . ∈ . : 'a × iset('a);
       . ⊆ . : iset('a) × iset('a);
   
   variables 
       s : iset('a);
       a : 'a;
       b : 'a;
       f : 'a → bool;
   
   
   induction 
      iset('a) generated by { };
   
   axioms 
      characteristic-function: χ(s)(a) ↔ a ∈ s;
      used for: s, ls;
      
      construct-set: a ∈ {f}  ↔ f(a);
      used for: s, ls;
      
      Extension: s1 = s2 ↔ (∀ a. a ∈ s1 ↔ a ∈ s2);
      used for: ls;
      
      In-empty: ¬ a ∈ ∅;
      used for: s, ls;
      
      In-insert: a ∈ s ++ b ↔ a = b ∨ a ∈ s;
      used for: s, ls;
      
      Subset: s1 ⊆ s2 ↔ (∀ a. a ∈ s1 → a ∈ s2);
      used for: ls;
   
   
end enrich