DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
5Thm*  Infinite(A Finite(A)[infinite_imp_nonfinite]
cites the following:
0Thm*  Infinite(A Unbounded(A)[unboundedly_imp_productively_infinite]
4Thm*  Unbounded(A Finite(A)[unb_inf_not_fin]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
DiscreteMath Sections DiscrMathExt Doc