Description: The maximum of two ordinals is equal to one of them. (Contributed by Mario Carneiro, 25-Jun-2015)