Theorem relation_union

Proof
01. 1 ⊢ relation R, hypo.
02. 2 ⊢ relation Q, hypo.
03. 1 ⊢ ∀t. t ∈ R → ∃x. ∃y. t = (x, y), relation_unfold 1.
04. 2 ⊢ ∀t. t ∈ Q → ∃x. ∃y. t = (x, y), relation_unfold 2.
05. 1 ⊢ t ∈ R → ∃x. ∃y. t = (x, y), uq_elim 3.
06. 2 ⊢ t ∈ Q → ∃x. ∃y. t = (x, y), uq_elim 4.
07. 7 ⊢ t ∈ R ∪ Q, hypo.
08. 7 ⊢ t ∈ R ∨ t ∈ Q, union_elim 7.
09. 9 ⊢ t ∈ R, hypo.
10. 1, 9 ⊢ ∃x. ∃y. t = (x, y), subj_elim 5 9.
11. 11 ⊢ t ∈ Q, hypo.
12. 2, 11 ⊢ ∃x. ∃y. t = (x, y), subj_elim 6 11.
13. 1, 2, 7 ⊢ ∃x. ∃y. t = (x, y), disj_elim 8 10 12.
14. 1, 2 ⊢ t ∈ R ∪ Q → ∃x. ∃y. t = (x, y), subj_intro 13.
15. 1, 2 ⊢ ∀t. t ∈ R ∪ Q → ∃x. ∃y. t = (x, y), uq_intro 14.
16. 1, 2 ⊢ relation (R ∪ Q), relation_fold 15.
relation_union. ⊢ relation R → relation Q → relation (R ∪ Q),
  subj_intro_ii 16.

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