Theorem union_incl_in_union

Proof
01. 1 ⊢ A1 ⊆ B1, hypo.
02. 2 ⊢ A2 ⊆ B2, hypo.
03. 3 ⊢ x ∈ A1 ∪ A2, hypo.
04. 3 ⊢ x ∈ A1 ∨ x ∈ A2, union_elim 3.
05. 5 ⊢ x ∈ A1, hypo.
06. 1, 5 ⊢ x ∈ B1, incl_elim 1 5.
07. 1, 5 ⊢ x ∈ B1 ∪ B2, union_introl 6.
08. 8 ⊢ x ∈ A2, hypo.
09. 2, 8 ⊢ x ∈ B2, incl_elim 2 8.
10. 2, 8 ⊢ x ∈ B1 ∪ B2, union_intror 9.
11. 1, 2, 3 ⊢ x ∈ B1 ∪ B2, disj_elim 4 7 10.
12. 1, 2 ⊢ x ∈ A1 ∪ A2 → x ∈ B1 ∪ B2, subj_intro 11.
13. 1, 2 ⊢ ∀x. x ∈ A1 ∪ A2 → x ∈ B1 ∪ B2, uq_intro 12.
14. 1, 2 ⊢ A1 ∪ A2 ⊆ B1 ∪ B2, incl_intro 13.
union_incl_in_union. ⊢ A1 ⊆ B1 → A2 ⊆ B2 → A1 ∪ A2 ⊆ B1 ∪ B2,
  subj_intro_ii 14.

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