Theorem setr_from_union

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

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