enrich
   set-basic
with
   functions 
       { . } : 'a → set('a);
       . ∪ . : set('a) × set('a) → set('a);
       . ∩ . : set('a) × set('a) → set('a);
       . \ . : set('a) × set('a) → set('a);
       . -- . : set('a) × 'a → set('a) prio 9 left;
       . map . : set('a) × ('a → 'b) → set('b);
       filter : set('a) × ('a → bool) → set('a);
   
   predicates 
       disjoint : set('a) × set('a);
   
   variables 
       s : set('a);
       a : 'a;
       b : 'b;
       f : 'a → 'b;
       p : 'a → bool;
   
   
   axioms 
      filter-in: a ∈ filter(s, p) ↔ a ∈ s ∧ p(a);
      used for: s, ls;
      
      map-base: ∅ map f = ∅;
      used for: s, ls;
      
      map-rec: ¬ a ∈ s → (s ++ a) map f = (s map f) ++ f(a);
      used for: s, ls;
      
      One: {a}  = ∅ ++ a;
      used for: ls;
      
      Union: a ∈ s1 ∪ s2 ↔ a ∈ s1 ∨ a ∈ s2;
      used for: s, ls;
      
      Intersect: a ∈ s1 ∩ s2 ↔ a ∈ s1 ∧ a ∈ s2;
      used for: s, ls;
      
      Difference: a ∈ s1 \ s2 ↔ a ∈ s1 ∧ ¬ a ∈ s2;
      used for: s, ls;
      
      Delete: a ∈ s -- a0 ↔ a ≠ a0 ∧ a ∈ s;
      used for: s, ls;
      
      Disjoint: s1 ∩ s2 = ∅ ↔ disjoint(s1, s2);
      used for: s, ls;
   
   
end enrich