Theorem composition_is_relation

Proof
01. 1 ⊢ t ∈ S ∘ R, hypo.
02. ⊢ S ∘ R = {t | ∃x. ∃y. ∃z. t = (x, z) ∧ (x, y) ∈ R ∧ (y, z) ∈ S},
  composition_eq.
03. 1 ⊢ t ∈ {t | ∃x. ∃y. ∃z. t = (x, z) ∧ (x, y) ∈ R ∧ (y, z) ∈ S},
  eq_subst 2 1, P u ↔ t ∈ u.
04. 1 ⊢ ∃x. ∃y. ∃z. t = (x, z) ∧ (x, y) ∈ R ∧ (y, z) ∈ S,
  comp_elim 3.
05. 5 ⊢ ∃y. ∃z. t = (x, z) ∧ (x, y) ∈ R ∧ (y, z) ∈ S, hypo.
06. 6 ⊢ ∃z. t = (x, z) ∧ (x, y) ∈ R ∧ (y, z) ∈ S, hypo.
07. 7 ⊢ t = (x, z) ∧ (x, y) ∈ R ∧ (y, z) ∈ S, hypo.
08. 7 ⊢ t = (x, z), conj_elimll 7.
09. 7 ⊢ ∃z. t = (x, z), ex_intro 8.
10. 7 ⊢ ∃x. ∃z. t = (x, z), ex_intro 9.
11. 6 ⊢ ∃x. ∃z. t = (x, z), ex_elim 6 10.
12. 5 ⊢ ∃x. ∃z. t = (x, z), ex_elim 5 11.
13. 1 ⊢ ∃x. ∃z. t = (x, z), ex_elim 4 12.
14. ⊢ t ∈ S ∘ R → ∃x. ∃z. t = (x, z), subj_intro 13.
15. ⊢ ∀t. t ∈ S ∘ R → ∃x. ∃z. t = (x, z), uq_intro 14.
composition_is_relation. ⊢ relation (S ∘ R), relation_fold 15.

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