Proof 01. 1 ⊢ univ U, hypo. 02. 1 ⊢ ∅ ∈ U, lsubj_conj_elimlll univ_equi 1. univ_contains_empty_set. ⊢ univ U → ∅ ∈ U, subj_intro 2.