Definition. union_eq
A ∪ B = {x | x ∈ A ∨ x ∈ B}