Theorem Ordinal.card_add

Modification history