Proof 01. 1 ⊢ x ∈ UnivCl, hypo. 02. 1 ⊢ set x, set_intro 1. UnivCl_elim. ⊢ x ∈ UnivCl → set x, subj_intro 2.