src/HOL/Cardinals/Cardinal_Order_Relation.thy

 lemma stable_nat: "stable |UNIV::nat set|"
 using stable_natLeq card_of_nat stable_ordIso by auto
 
 text{* Below, the type of "A" is not important -- we just had to choose an appropriate
    type to make "A" possible. What is important is that arbitrarily large
-   \<not>finite sets of stable cardinality exist. *}
+   infinite sets of stable cardinality exist. *}
 
 lemma infinite_stable_exists:
 assumes CARD: "\<forall>r \<in> R. Card_order (r::'a rel)"
 shows "\<exists>(A :: (nat + 'a set)set).
           \<not>finite A \<and> stable |A| \<and> (\<forall>r \<in> R. r <o |A| )"