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.