Definition. on_lt_equi
on_lt = {t | ∃α. ∃β. α ∈ On ∧ β ∈ On ∧ α ∈ β ∧ t = (α, β)}