incl_intro

Theorem. incl_intro
(∀x. x ∈ A → x ∈ B) → A ⊆ B

Proof
incl_intro. ⊢ (∀x. x ∈ A → x ∈ B) → A ⊆ B, bij_elimr incl_equi.