Proof 01. 1 ⊢ univ U, hypo. 02. 1 ⊢ (∀x. x ∈ U → x ⊆ U), lsubj_conj_elimllr univ_equi 1. 03. 1 ⊢ x ∈ U → x ⊆ U, uq_elim 2. univ_trans. ⊢ univ U → x ∈ U → x ⊆ U, subj_intro 3.