Theorem bij_from_inj_sur

Theorem. bij_from_inj_sur
inj f X Y → sur f X Y → bij f X Y
Proof
01. 1 ⊢ inj f X Y, hypo.
02. 2 ⊢ sur f X Y, hypo.
03. 1, 2 ⊢ inj f X Y ∧ sur f X Y, conj_intro 1 2.
04. 1, 2 ⊢ bij f X Y, rsubj_elim bij_equi 3.
bij_from_inj_sur. ⊢ inj f X Y → sur f X Y → bij f X Y,
  subj_intro_ii 4.