Finite-subset lifting of a well-quasi-order
= Finite-subset lifting of a well-quasi-order
Finite subsets of a <well-quasi-ordering>, compared by <Hoare domination preorder>, form a <well-quasi-ordering>. Enumerate each finite subset as a <word> and apply <Higman lemma>: a subsequence embedding with increased letters supplies a domination witness for every source element. This does not assert the same result for the full <power set>.