Theorem relation_subclass

Proof
01. 1 ⊢ R ⊆ Q, hypo.
02. 2 ⊢ relation Q, hypo.
03. 3 ⊢ t ∈ R, hypo.
04. 1, 3 ⊢ t ∈ Q, incl_elim 1 3.
05. 2 ⊢ ∀t. t ∈ Q → ∃x. ∃y. t = (x, y), relation_unfold 2.
06. 2 ⊢ t ∈ Q → ∃x. ∃y. t = (x, y), uq_elim 5.
07. 1, 2, 3 ⊢ ∃x. ∃y. t = (x, y), subj_elim 6 4.
08. 1, 2 ⊢ t ∈ R → ∃x. ∃y. t = (x, y), subj_intro 7.
09. 1, 2 ⊢ ∀t. t ∈ R → ∃x. ∃y. t = (x, y), uq_intro 8.
10. 1, 2 ⊢ relation R, relation_fold 9.
relation_subclass. ⊢ R ⊆ Q → relation Q → relation R, subj_intro_ii 10.