Theorem Intersection_dec

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

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