Theorem incl_trans

Theorem. incl_trans
A ⊆ B → B ⊆ C → A ⊆ C
Proof
01. 1 ⊢ A ⊆ B, hypo.
02. 2 ⊢ B ⊆ C, hypo.
03. 3 ⊢ x ∈ A, hypo.
04. 1, 3 ⊢ x ∈ B, incl_elim 1 3.
05. 1, 2, 3 ⊢ x ∈ C, incl_elim 2 4.
06. 1, 2 ⊢ x ∈ A → x ∈ C, subj_intro 5.
07. 1, 2 ⊢ ∀x. x ∈ A → x ∈ C, uq_intro 6.
08. 1, 2 ⊢ A ⊆ C, incl_intro 7.
incl_trans. ⊢ A ⊆ B → B ⊆ C → A ⊆ C, subj_intro_ii 8.