Ordinals_and_Cardinals.Cardinal_Order_Relation_discontinued