enrich
infset-union
with
functions χ : set → elem → bool;
{ . } : (elem → bool) → set;
variables f : elem → bool;
axioms characteristic-function : ⊦ χ(s)(a) ↔ a ∈ s;
used for: s, ls;
construct-set : ⊦ a ∈ {f} ↔ f(a);
used for: s, ls;
end enrich