Due to the type system of HLM, it is impossible to define the union of two arbitrary sets. Instead, both sets must be declared as subsets of a common superset U, although the union is, of course, independent of U. Since a suitable value for U can always be inferred automatically, U can be omitted from the notation.