Theorem union_intror

Proof
01. 1 ⊢ x ∈ B, hypo.
02. 1 ⊢ x ∈ A ∨ x ∈ B, disj_intror 1.
03. 1 ⊢ x ∈ A ∪ B, union_intro 2.
union_intror. ⊢ x ∈ B → x ∈ A ∪ B, subj_intro 3.

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