Theorem transitive_closed_Intersection

Proof
01. 1 ⊢ ∀x. x ∈ M → transitive x, hypo.
02. 2 ⊢ u ∈ ⋂M, hypo.
03. 3 ⊢ y ∈ u, hypo.
04. 4 ⊢ x ∈ M, hypo.
05. 1, 4 ⊢ transitive x, uq_bounded_elim 1 4.
06. 2, 4 ⊢ u ∈ x, Intersection_elim 2 4.
07. 1, 2, 4 ⊢ u ⊆ x, transitive_elim 5 6.
08. 1, 2, 3, 4 ⊢ y ∈ x, incl_elim 7 3.
09. 1, 2, 3 ⊢ x ∈ M → y ∈ x, subj_intro 8.
10. 1, 2, 3 ⊢ ∀x. x ∈ M → y ∈ x, uq_intro 9.
11. 3 ⊢ set y, set_intro 3.
12. 1, 2, 3 ⊢ y ∈ ⋂M, Intersection_intro 11 10.
13. 1, 2 ⊢ y ∈ u → y ∈ ⋂M, subj_intro 12.
14. 1, 2 ⊢ ∀y. y ∈ u → y ∈ ⋂M, uq_intro 13.
15. 1, 2 ⊢ u ⊆ ⋂M, incl_intro 14.
16. 1 ⊢ u ∈ ⋂M → u ⊆ ⋂M, subj_intro 15.
17. 1 ⊢ ∀u. u ∈ ⋂M → u ⊆ ⋂M, uq_intro 16.
18. 1 ⊢ transitive (⋂M), transitive_intro 17.
transitive_closed_Intersection. ⊢
  (∀x. x ∈ M → transitive x) → transitive (⋂M), subj_intro 18.

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