sur_elim

Theorem. sur_elim
sur f X Y → rng f = Y

Proof
01. 1 ⊢ sur f X Y, hypo.
02. 1 ⊢ rng f = Y, lsubj_conj_elimr sur_equi 1.
sur_elim. ⊢ sur f X Y → rng f = Y, subj_intro 2.