Theorem non_empty_from_witness

Proof
01. 1 ⊢ x ∈ A, hypo.
02. 2 ⊢ A = ∅, hypo.
03. 1, 2 ⊢ x ∈ ∅, eq_subst 2 1.
04. 1, 2 ⊢ ⊥, empty_contra 3.
05. 1 ⊢ ¬A = ∅, neg_intro 4.
non_empty_from_witness. ⊢ x ∈ A → ¬A = ∅,
  subj_intro 5.

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