Theorem Intersection_intro_non_empty

Proof
01. 1 ⊢ ¬M = ∅, hypo.
02. 2 ⊢ ∀y. y ∈ M → x ∈ y, hypo.
03. 1 ⊢ ∃y. y ∈ M, non_empty 1.
04. 4 ⊢ y ∈ M, hypo.
05. 2 ⊢ y ∈ M → x ∈ y, uq_elim 2.
06. 2, 4 ⊢ x ∈ y, subj_elim 5 4.
07. 2, 4 ⊢ set x, set_intro 6.
08. 1, 2 ⊢ set x, ex_elim 3 7.
09. 1, 2 ⊢ x ∈ ⋂M, Intersection_intro 8 2.
Intersection_intro_non_empty. ⊢ ¬M = ∅ →
  (∀y. y ∈ M → x ∈ y) → x ∈ ⋂M, subj_intro_ii 9.

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