% Alternate axiomatization of sets

set name set

declare sorts Elem, Set
declare variables 
  e, e':     Elem
  x, y, z:   Set
  ..
declare operators
  {}:                      -> Set
  {__}:          Elem      -> Set
  __\union__:    Set, Set  -> Set
  __\in__:       Elem, Set -> Bool
  insert:        Elem, Set -> Set
  __\subseteq__: Set, Set  -> Bool
  ..

% Axioms

assert 
  ac \union;
  sort Set generated by {}, {__}, \union;
  sort Set partitioned by \in;
  ~(e \in {});
  e \in {e'} <=> e = e';
  e \in (x \union y) <=> e \in x \/ e \in y;
  insert(e, x) = {e} \union x;
  {} \subseteq x;
  {e} \subseteq x <=> e \in x;
  (x \union y) \subseteq z <=> x \subseteq z /\ y \subseteq z
  ..