Definition. diag_rl_eq
diag_rl = {t | ∃x. ∃y. t = (x, y) ∧ x ∈ y}