Theorem setl_from_union

Proof
01. ⊢ A ⊆ A ∪ B, union_incl_left.
02. ⊢ A ⊆ A ∪ B → set (A ∪ B) → set A, subset.
setl_from_union. ⊢ set (A ∪ B) → set A, subj_elim 2 1.

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