Proof 01. 1 ⊢ bij f X Y, hypo. 02. 1 ⊢ inj f X Y, lsubj_conj_eliml bij_equi 1. bij_is_inj. ⊢ bij f X Y → inj f X Y, subj_intro 2.