Def  Dedekind-Infinite(A) == a:A, f:(AA). Inj(A; A; f) & (x:A. f(x) = a)

is mentioned by

Thm*  Dedekind-Infinite(A)  Finite(A)	[dedekind_imp_nonfin]
Thm*  Dedekind-Infinite(A)  Unbounded(A)	[dededing_imp_unb_inf]
Thm*  Dedekind-Infinite(A)  Infinite(A)	[dedekind_inf_imp_inf]
Thm*  (A ~ B)  Dedekind-Infinite(A)  Dedekind-Infinite(B)	[ooc_preserves_dededkind_inf]

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html