Definition. On_eq
On = Univ ∩ {α | transitive α ∧ ∀x. x ∈ α → transitive x}