Proof 01. 1 ⊢ bij f X Y, hypo. 02. 1 ⊢ sur f X Y, lsubj_conj_elimr bij_equi 1. bij_is_sur. ⊢ bij f X Y → sur f X Y, subj_intro 2.