Definition Intersection_eq

Definition. Intersection_eq
⋂M = {x | ∀A. A ∈ M → x ∈ A}

The intersection of a class of sets. Note that M is allowed to be empty, then ⋂M is UnivCl, as Intersection_empty_set shows.