Proof 01. 1 ⊢ relation R, hypo. 02. 2 ⊢ t ∈ R, hypo. 03. 1 ⊢ ∀t. t ∈ R → ∃x. ∃y. t = (x, y), relation_unfold 1. 04. 1, 2 ⊢ ∃x. ∃y. t = (x, y), uq_bounded_elim 3 2. relation_elim. ⊢ relation R → t ∈ R → ∃x. ∃y. t = (x, y), subj_intro_ii 4.