Theorem empty_contra

Proof
01. 1 ⊢ x ∈ ∅, hypo.
02. 1 ⊢ x ∈ {x | ⊥}, eq_subst empty_set_eq 1.
03. 1 ⊢ ⊥, comp_elim 2.
empty_contra. ⊢ x ∈ ∅ → ⊥, subj_intro 3.

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