Definition. inv_img_eq
inv_img R B = {x | ∃y. y ∈ B ∧ (x, y) ∈ R}