Theorem union_compl

Proof
01. 1 ⊢ x ∈ UnivCl, hypo.
02. 1 ⊢ set x, set_intro 1.
03. ⊢ x ∈ A ∨ ¬x ∈ A, lem.
04. 4 ⊢ x ∈ A, hypo.
05. 4 ⊢ x ∈ A ∪ compl A, union_introl 4.
06. 6 ⊢ ¬x ∈ A, hypo.
07. 1, 6 ⊢ x ∈ compl A, compl_intro 2 6.
08. 1, 6 ⊢ x ∈ A ∪ compl A, union_intror 7.
09. 1 ⊢ x ∈ A ∪ compl A, disj_elim 3 5 8.
10. ⊢ x ∈ UnivCl → x ∈ A ∪ compl A, subj_intro 9.
11. ⊢ ∀x. x ∈ UnivCl → x ∈ A ∪ compl A, uq_intro 10.
12. ⊢ UnivCl ⊆ A ∪ compl A, incl_intro 11.
13. ⊢ A ∪ compl A ⊆ UnivCl, UnivCl_is_greatest.
union_compl. ⊢ A ∪ compl A = UnivCl, incl_antisym 13 12.

Dependencies
The given proof depends on five axioms:
comp, eq_refl, eq_subst, ext, lem.