Proof 01. 1 ⊢ transitive x, hypo. 02. 1 ⊢ ∀u. u ∈ x → u ⊆ x, lsubj_elim transitive_equi 1. 03. 1 ⊢ u ∈ x → u ⊆ x, uq_elim 2. transitive_elim. ⊢ transitive x → u ∈ x → u ⊆ x, subj_intro 3.