Theorem lower_bound_incl_in_Intersection

Proof
01. 1 ⊢ ∀x. x ∈ M → u ⊆ x, hypo.
02. 2 ⊢ y ∈ u, hypo.
03. 3 ⊢ x ∈ M, hypo.
04. 1, 3 ⊢ u ⊆ x, uq_bounded_elim 1 3.
05. 1, 2, 3 ⊢ y ∈ x, incl_elim 4 2.
06. 1, 2 ⊢ x ∈ M → y ∈ x, subj_intro 5.
07. 1, 2 ⊢ ∀x. x ∈ M → y ∈ x, uq_intro 6.
08. 2 ⊢ set y, set_intro 2.
09. 1, 2 ⊢ y ∈ ⋂M, Intersection_intro 8 7.
10. 1 ⊢ y ∈ u → y ∈ ⋂M, subj_intro 9.
11. 1 ⊢ ∀y. y ∈ u → y ∈ ⋂M, uq_intro 10.
12. 1 ⊢ u ⊆ ⋂M, incl_intro 11.
lower_bound_incl_in_Intersection. ⊢ (∀x. x ∈ M → u ⊆ x) → u ⊆ ⋂M,
  subj_intro 12.

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