relation_unfold

Theorem. relation_unfold
relation R → ∀t. t ∈ R → ∃x. ∃y. t = (x, y)

Proof
relation_unfold. ⊢ relation R → ∀t. t ∈ R → ∃x. ∃y. t = (x, y),
  bij_eliml relation_equi.