Theorem compl_elim

Proof
01. 1 ⊢ x ∈ compl A, hypo.
02. 1 ⊢ x ∈ {x | ¬x ∈ A}, eq_subst compl_eq 1, P u ↔ x ∈ u.
03. 1 ⊢ ¬x ∈ A, comp_elim 2.
compl_elim. ⊢ x ∈ compl A → ¬x ∈ A, subj_intro 3.

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