num_eq_intro

Theorem. num_eq_intro
(∃f. bij f X Y) → num_eq X Y

Proof
num_eq_intro. ⊢ (∃f. bij f X Y) → num_eq X Y,
  bij_elimr num_eq_equi.