Theorem UnivCl_is_greatest

Proof
01. 1 ⊢ x ∈ A, hypo.
02. 1 ⊢ set x, set_intro 1.
03. 1 ⊢ x ∈ UnivCl, UnivCl_intro 2.
04. ⊢ x ∈ A → x ∈ UnivCl, subj_intro 3.
05. ⊢ ∀x. x ∈ A → x ∈ UnivCl, uq_intro 4.
UnivCl_is_greatest. ⊢ A ⊆ UnivCl, incl_intro 5.

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