Theorem relation_incl_prod

Proof
1. 1 ⊢ relation R, hypo.
2. 2 ⊢ dom R ⊆ X, hypo.
3. 3 ⊢ rng R ⊆ Y, hypo.
4. 4 ⊢ t ∈ R, hypo.
5. 1 ⊢ ∀t. t ∈ R → ∃x. ∃y. t = (x, y), relation_unfold 1.
6. 1 ⊢ t ∈ R → ∃x. ∃y. t = (x, y), uq_elim 5.
7. 1, 4 ⊢ ∃x. ∃y. t = (x, y), subj_elim 6 4.
8. 8 ⊢ ∃y. t = (x, y), hypo.
9. 9 ⊢ t = (x, y), hypo.
10. 4, 9 ⊢ (x, y) ∈ R, eq_subst 9 4, P u ↔ u ∈ R.
11. 4, 9 ⊢ x ∈ dom R, dom_intro 10.
12. 2, 4, 9 ⊢ x ∈ X, incl_elim 2 11.
13. 4, 9 ⊢ y ∈ rng R, rng_intro 10.
14. 3, 4, 9 ⊢ y ∈ Y, incl_elim 3 13.
15. 2, 3, 4, 9 ⊢ (x, y) ∈ X × Y, prod_intro 12 14.
16. 2, 3, 4, 9 ⊢ t ∈ X × Y, eq_subst_rev 9 15, P u ↔ u ∈ X × Y.
17. 2, 3, 4, 8 ⊢ t ∈ X × Y, ex_elim 8 16.
18. 1, 2, 3, 4 ⊢ t ∈ X × Y, ex_elim 7 17.
19. 1, 2, 3 ⊢ t ∈ R → t ∈ X × Y, subj_intro 18.
20. 1, 2, 3 ⊢ ∀t. t ∈ R → t ∈ X × Y, uq_intro 19.
21. 1, 2, 3 ⊢ R ⊆ X × Y, incl_intro 20.
relation_incl_prod. ⊢ relation R →
  dom R ⊆ X → rng R ⊆ Y → R ⊆ X × Y, subj_intro_iii 21.

Dependencies
The given proof depends on nine axioms:
comp, efq, eq_refl, eq_subst, ext, lem, pairing, subset, union.