Description: Intersection of total order with Cartesian product of its field. (Contributed by Mario Carneiro, 10-Jul-2014)