Theorem UnivCl_is_proper

Proof
01. 1 ⊢ x ∈ DiagCl, hypo.
02. 1 ⊢ set x, set_intro 1.
03. 1 ⊢ x ∈ UnivCl, UnivCl_intro 2.
04. ⊢ x ∈ DiagCl → x ∈ UnivCl, subj_intro 3.
05. ⊢ ∀x. x ∈ DiagCl → x ∈ UnivCl, uq_intro 4.
06. ⊢ DiagCl ⊆ UnivCl, incl_intro 5.
07. ⊢ DiagCl ⊆ UnivCl → set UnivCl → set DiagCl, subset.
08. ⊢ set UnivCl → set DiagCl, subj_elim 7 6.
09. 9 ⊢ set UnivCl, hypo.
10. 9 ⊢ set DiagCl, subj_elim 8 9.
11. 9 ⊢ ⊥, neg_elim DiagCl_is_proper 10.
UnivCl_is_proper. ⊢ ¬set UnivCl, neg_intro 11.

Dependencies
The given proof depends on four axioms:
comp, eq_refl, eq_subst, subset.