Theorem incl_elim

Theorem. incl_elim
A ⊆ B → x ∈ A → x ∈ B
Proof
01. ⊢ A ⊆ B → (∀x. x ∈ A → x ∈ B), bij_eliml incl_equi.
02. 2 ⊢ A ⊆ B, hypo.
03. 2 ⊢ ∀x. x ∈ A → x ∈ B, subj_elim 1 2.
04. 2 ⊢ x ∈ A → x ∈ B, uq_elim 3.
incl_elim. ⊢ A ⊆ B → x ∈ A → x ∈ B, subj_intro 4.