Theorem transitive_intro
Theorem.
transitive_intro
(∀u. u ∈ x → u ⊆ x) → transitive x
Proof
transitive_intro. ⊢ (∀u. u ∈ x → u ⊆ x) → transitive x,
rsubj_elim
transitive_equi
.