In set theory, a prewellordering is a binary relation \le that is transitive, total, and wellfounded (more precisely, the relation x\le y\land y\nleq x is wellfounded). In other words, if \leq is a prewellordering on a set X, and if we define \sim by