Definition 1.1.8.  Let U be a set, S, T ⊆ U. We define:
S ∩ T:= {x ∈ U : x ∈ S and x ∈ T}

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