Theorem univ_closed_Intersection

Proof
01. 1 ⊢ univ U, hypo.
02. 2 ⊢ M ∈ U, hypo.
03. 3 ⊢ ¬M = ∅, hypo.
04. 3 ⊢ ∃y. y ∈ M, non_empty 3.
05. 5 ⊢ y ∈ M, hypo.
06. ⊢ ⋂M = ⋂M, eq_refl.
07. 5 ⊢ ⋂M ⊆ y, Intersection_is_lower_bound 6 5.
08. 1, 2 ⊢ M ⊆ U, univ_trans 1 2.
09. 1, 2, 5 ⊢ y ∈ U, incl_elim 8 5.
10. 1, 2, 5 ⊢ ⋂M ∈ U, univ_closed_subset 1 7 9.
11. 1, 2, 3 ⊢ ⋂M ∈ U, ex_elim 4 10.
univ_closed_Intersection. ⊢ univ U → M ∈ U → ¬M = ∅ → ⋂M ∈ U,
  subj_intro_iii 11.

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