Theorem diff_incl

Proof
01. 1 ⊢ x ∈ A \ B, hypo.
02. 1 ⊢ x ∈ A, diff_eliml 1.
03. ⊢ x ∈ A \ B → x ∈ A, subj_intro 2.
04. ⊢ ∀x. x ∈ A \ B → x ∈ A, uq_intro 3.
diff_incl. ⊢ A \ B ⊆ A, incl_intro 4.

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