DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
6Thm*  Dedekind-Infinite(A Finite(A)[dedekind_imp_nonfin]
cites the following:
5Thm*  Infinite(A Finite(A)[infinite_imp_nonfinite]
3Thm*  Dedekind-Infinite(A Infinite(A)[dedekind_inf_imp_inf]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
DiscreteMath Sections DiscrMathExt Doc