Theorem relation_from_incl

Proof
01. 1 ⊢ R ⊆ X × Y, hypo.
02. 2 ⊢ t ∈ R, hypo.
03. 1, 2 ⊢ t ∈ X × Y, incl_elim 1 2.
04. 1, 2 ⊢ ∃x. ∃y. x ∈ X ∧ y ∈ Y ∧ t = (x, y), prod_elim 3.
05. 5 ⊢ ∃y. x ∈ X ∧ y ∈ Y ∧ t = (x, y), hypo.
06. 6 ⊢ x ∈ X ∧ y ∈ Y ∧ t = (x, y), hypo.
07. 6 ⊢ t = (x, y), conj_elimr 6.
08. 6 ⊢ ∃y. t = (x, y), ex_intro 7.
09. 6 ⊢ ∃x. ∃y. t = (x, y), ex_intro 8.
10. 5 ⊢ ∃x. ∃y. t = (x, y), ex_elim 5 9.
11. 1, 2 ⊢ ∃x. ∃y. t = (x, y), ex_elim 4 10.
12. 1 ⊢ t ∈ R → ∃x. ∃y. t = (x, y), subj_intro 11.
13. 1 ⊢ ∀t. t ∈ R → ∃x. ∃y. t = (x, y), uq_intro 12.
14. ⊢ (∀t. t ∈ R → ∃x. ∃y. t = (x, y)) → relation R,
  bij_elimr relation_equi.
15. 1 ⊢ relation R, subj_elim 14 13.
relation_from_incl. ⊢ R ⊆ X × Y → relation R, subj_intro 15.

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