for X being set ex R being Relation st R well_orders X