Description: Thus, there is at most one isomorphism between any two well-ordered sets. TODO: Shorten finnisoeu . (Contributed by Stefan O'Rear, 12-Feb-2015) (Revised by Mario Carneiro, 25-Jun-2015)