Definition. transitive_equi
transitive x ↔ ∀u. u ∈ x → u ⊆ x